all trigger the bug. Therefore, I have -- unfortunately -- chosen
definitions which avoid product categories and bifunctors wherever
possible.
+
+IMPORTANT NOTE ABOUT SUBCATEGORIES: non-wide subcategories (that is,
+subcategories which do not include all objects of the parent category)
+are awkward to handle in Coq. This is because they unavoidably
+involve reasoning about equality of objects, and objects are the
+indices of the types of hom-sets. Coq is not very good at dealing
+with equality between types which are the indices of other types. For
+this reason, I have two kinds of subcategory: WideSubcategory (which
+behaves quite nicely) and FullSubcategory (which can cause problems).
+Every subcategory of C is a full subcategory of a wide subcategory of
+C, and you must formalize it this way.
Coercion UnderlyingFunctor : EFunctor >-> Functor.
Class EBinoidalCat `(ec:ECategory) :=
-{ ebc_bobj : ec -> ec -> ec
-; ebc_first : forall a:ec, EFunctor ec ec (fun x => ebc_bobj x a)
-; ebc_second : forall a:ec, EFunctor ec ec (fun x => ebc_bobj a x)
+{ ebc_bobj : ec -> ec -> ec
+; ebc_first : forall a:ec, EFunctor ec ec (fun x => ebc_bobj x a)
+; ebc_second : forall a:ec, EFunctor ec ec (fun x => ebc_bobj a x)
+; ebc_ec := ec (* this isn't a coercion - avoids duplicate paths *)
}.
Instance EBinoidalCat_is_binoidal `(ebc:EBinoidalCat(ec:=ec)) : BinoidalCat (Underlying ec) ebc_bobj.
(* A Freyd Category is... *)
Class FreydCategory
- (* a cartesian category C *)
- `(C:CartesianCat(Ob:=Ob)(C:=C1))
+ (* a cartesian category C *)
+ `(C:CartesianCat(Ob:=Ob)(C:=C1)(bin_obj':=bobj))
- (* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *)
+ (* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *)
`(K:PreMonoidalCat(Ob:=Ob)(bin_obj':=bobj)(I:=@one _ _ _ C))
- (* an identity-on-objects functor J:C->Z(K) *)
-:= { fc_J : Functor C (Center_is_Monoidal K) (fun x => exist (fun _ => True) x I)
+ (* an identity-on-objects functor J:C->Z(K) *)
+:= { fc_J : Functor C (Center_is_Monoidal K) (fun x => x)
- (* which is not only monoidal *)
+ (* which is a monoidal functor *)
; fc_mf_J : MonoidalFunctor C (Center_is_Monoidal K) fc_J
- (* but in fact strict (meaning the functor's coherence maps are identities) *)
- (*; fc_strict : forall a b, #(mf_first a b) ~~ id _
- FIXME - I will need to separate Subcategory from FullSubCategory in order to fix this *)
+ (* and strict (meaning the functor's coherence maps are identities) *)
+ ; fc_strict_first : forall a b, #(mf_first(PreMonoidalFunctor:=fc_mf_J) a b) ~~ id _ (* mf_consistent gives us mf_second *)
+(* ; fc_strict_id : #(mf_i(PreMonoidalFunctor:=fc_mf_J)) ~~ id _*)
; fc_C := C
; fc_K := K
+++ /dev/null
-(******************************************************************************)
-(* General Data Structures *)
-(******************************************************************************)
-
-Require Import Coq.Unicode.Utf8.
-Require Import Coq.Classes.RelationClasses.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.Strings.String.
-Require Setoid.
-Require Import Coq.Lists.List.
-Require Import Preamble.
-Generalizable All Variables.
-Require Import Omega.
-
-
-Class EqDecidable (T:Type) :=
-{ eqd_type := T
-; eqd_dec : forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
-; eqd_dec_reflexive : forall v, (eqd_dec v v) = (left _ (refl_equal _))
-}.
-Coercion eqd_type : EqDecidable >-> Sortclass.
-
-
-(*******************************************************************************)
-(* Trees *)
-
-Inductive Tree (a:Type) : Type :=
- | T_Leaf : a -> Tree a
- | T_Branch : Tree a -> Tree a -> Tree a.
-Implicit Arguments T_Leaf [ a ].
-Implicit Arguments T_Branch [ a ].
-
-Notation "a ,, b" := (@T_Branch _ a b) : tree_scope.
-
-(* tree-of-option-of-X comes up a lot, so we give it special notations *)
-Notation "[ q ]" := (@T_Leaf (option _) (Some q)) : tree_scope.
-Notation "[ ]" := (@T_Leaf (option _) None) : tree_scope.
-Notation "[]" := (@T_Leaf (option _) None) : tree_scope.
-
-Open Scope tree_scope.
-
-Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
- match t with
- | T_Leaf x => T_Leaf (f x)
- | T_Branch l r => T_Branch (mapTree f l) (mapTree f r)
- end.
-Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
- match t with
- | T_Leaf None => T_Leaf None
- | T_Leaf (Some x) => T_Leaf (Some (f x))
- | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r)
- end.
-Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
- match t with
- | T_Leaf x => f x
- | T_Branch l r => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r)
- end.
-Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b :=
- match t with
- | T_Leaf None => []
- | T_Leaf (Some x) => f x
- | T_Branch l r => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r)
- end.
-Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) :=
- match t with
- | T_Leaf x => mapLeaf x
- | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z)
- end.
-Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
- forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
-
-Lemma tree_dec_eq :
- forall {Q}(t1 t2:Tree ??Q),
- (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) ->
- sumbool (t1=t2) (not (t1=t2)).
- intro Q.
- intro t1.
- induction t1; intros.
-
- destruct a; destruct t2.
- destruct o.
- set (X q q0) as X'.
- inversion X'; subst.
- left; auto.
- right; unfold not; intro; apply H. inversion H0; subst. auto.
- right. unfold not; intro; inversion H.
- right. unfold not; intro; inversion H.
- destruct o.
- right. unfold not; intro; inversion H.
- left; auto.
- right. unfold not; intro; inversion H.
-
- destruct t2.
- right. unfold not; intro; inversion H.
- set (IHt1_1 t2_1 X) as X1.
- set (IHt1_2 t2_2 X) as X2.
- destruct X1; destruct X2; subst.
- left; auto.
-
- right.
- unfold not; intro H.
- apply n.
- inversion H; auto.
-
- right.
- unfold not; intro H.
- apply n.
- inversion H; auto.
-
- right.
- unfold not; intro H.
- apply n.
- inversion H; auto.
- Defined.
-
-
-
-
-(*******************************************************************************)
-(* Lists *)
-
-Notation "a :: b" := (cons a b) : list_scope.
-Open Scope list_scope.
-Fixpoint leaves {a:Type}(t:Tree (option a)) : list a :=
- match t with
- | (T_Leaf l) => match l with
- | None => nil
- | Some x => x::nil
- end
- | (T_Branch l r) => app (leaves l) (leaves r)
- end.
-(* weak inverse of "leaves" *)
-Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) :=
- match l with
- | nil => []
- | (a::b) => [a],,(unleaves b)
- end.
-
-(* a map over a list and the conjunction of the results *)
-Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
- match l with
- | nil => True
- | (a::al) => f a /\ mapProp f al
- end.
-
-Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
- induction l.
- auto.
- simpl.
- rewrite IHl.
- auto.
- Defined.
-Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l').
- intros.
- induction l; auto.
- simpl.
- rewrite IHl.
- auto.
- Defined.
-Lemma map_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
- (map (g ○ f) l) = (map g (map f l)).
- intros.
- induction l.
- simpl; auto.
- simpl.
- rewrite IHl.
- auto.
- Defined.
-Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False.
- intros.
- induction b.
- inversion H.
- inversion H. apply IHb in H2.
- auto.
- Defined.
-Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False.
- induction b.
- intros; inversion H.
- intros.
- inversion H.
- apply IHb in H2.
- auto.
- Defined.
-
-Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[].
- intros.
- destruct h.
- destruct o. inversion H.
- auto.
- inversion H.
- Defined.
-
-Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q.
- induction q.
- destruct a0; simpl.
- reflexivity.
- reflexivity.
- simpl.
- rewrite IHq1.
- rewrite IHq2.
- reflexivity.
- Qed.
-
-(* handy facts: map preserves the length of a list *)
-Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
- intros.
- induction s1.
- auto.
- assert False.
- simpl in H.
- inversion H.
- inversion H0.
- Defined.
-Lemma map_on_singleton : forall A B (f:A->B) x (s1:list A), (cons x nil) = map f s1 -> { y : A & s1=(cons y nil) & (f y)=x }.
- induction s1.
- intros.
- simpl in H; assert False. inversion H. inversion H0.
- clear IHs1.
- intros.
- exists a.
- simpl in H.
- assert (s1=nil).
- inversion H. apply map_on_nil in H2. auto.
- subst.
- auto.
- assert (s1=nil).
- inversion H. apply map_on_nil in H2. auto.
- subst.
- simpl in H.
- inversion H. auto.
- Defined.
-
-Lemma map_on_doubleton : forall A B (f:A->B) x y (s1:list A), ((x::y::nil) = map f s1) ->
- { z : A*A & s1=((fst z)::(snd z)::nil) & (f (fst z))=x /\ (f (snd z))=y }.
- intros.
- destruct s1.
- inversion H.
- destruct s1.
- inversion H.
- destruct s1.
- inversion H.
- exists (a,a0); auto.
- simpl in H.
- inversion H.
- Defined.
-
-
-Lemma mapTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree A),
- (mapTree (g ○ f) l) = (mapTree g (mapTree f l)).
- induction l.
- reflexivity.
- simpl.
- rewrite IHl1.
- rewrite IHl2.
- reflexivity.
- Defined.
-
-Lemma lmap_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
- (map (g ○ f) l) = (map g (map f l)).
- intros.
- induction l.
- simpl; auto.
- simpl.
- rewrite IHl.
- auto.
- Defined.
-
-(* sends a::b::c::nil to [[[[],,c],,b],,a] *)
-Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) :=
- match l with
- | nil => []
- | (a::b) => (unleaves' b),,[a]
- end.
-
-(* sends a::b::c::nil to [[[[],,c],,b],,a] *)
-Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
- match l with
- | nil => []
- | (a::b) => (unleaves'' b),,(T_Leaf a)
- end.
-
-Fixpoint filter {T:Type}(l:list ??T) : list T :=
- match l with
- | nil => nil
- | (None::b) => filter b
- | ((Some x)::b) => x::(filter b)
- end.
-
-Inductive distinct {T:Type} : list T -> Prop :=
-| distinct_nil : distinct nil
-| distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
-
-Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
- induction l; auto.
- simpl.
- omega.
- Qed.
-
-(* decidable quality on a list of elements which have decidable equality *)
-Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
- sumbool (eq l1 l2) (not (eq l1 l2)).
- intro T.
- intro l1.
- induction l1; intros.
- destruct l2.
- left; reflexivity.
- right; intro H; inversion H.
- destruct l2 as [| b l2].
- right; intro H; inversion H.
- set (IHl1 l2 dec) as eqx.
- destruct eqx.
- subst.
- set (dec a b) as eqy.
- destruct eqy.
- subst.
- left; reflexivity.
- right. intro. inversion H. subst. apply n. auto.
- right.
- intro.
- inversion H.
- apply n.
- auto.
- Defined.
-
-
-
-
-(*******************************************************************************)
-(* Length-Indexed Lists *)
-
-Inductive vec (A:Type) : nat -> Type :=
-| vec_nil : vec A 0
-| vec_cons : forall n, A -> vec A n -> vec A (S n).
-
-Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
- match v with
- | vec_nil => nil
- | vec_cons n a va => a::(vec2list va)
- end.
-
-Require Import Omega.
-Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
- intro T.
- intro len.
- intro v.
- induction v; intros.
- assert False.
- inversion pf.
- inversion H.
- rename n into len.
- destruct n0 as [|n].
- exact a.
- apply (IHv n).
- omega.
- Defined.
-
-Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
- induction n.
- apply vec_nil.
- inversion va; subst.
- inversion vb; subst.
- apply vec_cons; auto.
- Defined.
-
-Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
- induction n.
- apply vec_nil.
- inversion v; subst.
- apply vec_cons; auto.
- Defined.
-
-Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
- match l with
- | vec_nil => False
- | vec_cons _ n m => (n = a) \/ vec_In a m
- end.
-Implicit Arguments vec_nil [ A ].
-Implicit Arguments vec_cons [ A n ].
-
-Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
- induction n.
- apply (vec_cons t vec_nil).
- apply vec_cons; auto.
- Defined.
-
-Definition list2vec {T:Type}(l:list T) : vec T (length l).
- induction l.
- apply vec_nil.
- apply vec_cons; auto.
- Defined.
-
-Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
- inversion v; auto.
- Defined.
-Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
- inversion v; auto.
- Defined.
-
-Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
- induction l1.
- apply vec_nil.
- apply vec_cons.
- simpl in *.
- inversion v; subst; auto.
- apply IHl1.
- inversion v; subst; auto.
- Defined.
-
-Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
- induction l1.
- apply v.
- simpl in *.
- apply IHl1; clear IHl1.
- inversion v; subst; auto.
- Defined.
-
-Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
-
-
-
-(*******************************************************************************)
-(* Shaped Trees *)
-
-(* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *)
-Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type :=
-| st_nil : @ShapedTree T Q []
-| st_leaf : forall {t}, Q -> @ShapedTree T Q [t]
-| st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2).
-
-Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
-match st with
-| st_nil => []
-| st_leaf _ q => [q]
-| st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
-end.
-
-Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
- induction st.
- apply st_nil.
- apply st_leaf. apply f. apply q.
- apply st_branch; auto.
- Defined.
-
-Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T}
- (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx.
- induction idx.
- destruct a.
- apply st_leaf; auto.
- inversion st1.
- inversion st2.
- auto.
- apply st_nil.
- apply st_branch; auto.
- inversion st1; subst; apply IHidx1; auto.
- inversion st2; subst; auto.
- inversion st2; subst; apply IHidx2; auto.
- inversion st1; subst; auto.
- Defined.
-
-Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
- induction idx.
- destruct a.
- apply st_leaf; auto.
- apply st_nil.
- apply st_branch; auto.
- Defined.
-
-Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx),
- mapOptionTree f (unshape t) = unshape (mapShapedTree f t).
- intros.
- induction t; auto.
- simpl.
- rewrite IHt1.
- rewrite IHt2.
- reflexivity.
- Qed.
-
-
-
-
-(*******************************************************************************)
-(* Type-Indexed Lists *)
-
-(* an indexed list *)
-Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
-| INil : IList I F nil
-| ICons : forall i is, F i -> IList I F is -> IList I F (i::is).
-Implicit Arguments INil [ I F ].
-Implicit Arguments ICons [ I F ].
-
-(* a tree indexed by a (Tree (option X)) *)
-Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
-| INone : ITree I F []
-| ILeaf : forall i: I, F i -> ITree I F [i]
-| IBranch : forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
-Implicit Arguments INil [ I F ].
-Implicit Arguments ILeaf [ I F ].
-Implicit Arguments IBranch [ I F ].
-
-
-
-
-(*******************************************************************************)
-(* Extensional equality on functions *)
-
-Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
-Hint Transparent extensionality.
-Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
- intros; apply Build_Equivalence;
- intros; compute; intros; auto.
- rewrite H; rewrite H0; auto.
- Defined.
- Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
- with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
- unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
- Defined.
-Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
- (extensionality _ _ f f') ->
- (extensionality _ _ g g') ->
- (extensionality _ _ (g ○ f) (g' ○ f')).
- intros.
- unfold extensionality.
- unfold extensionality in H.
- unfold extensionality in H0.
- intros.
- rewrite H.
- rewrite H0.
- auto.
- Qed.
-
-
-
-
-
-
-(* the Error monad *)
-Inductive OrError (T:Type) :=
-| Error : forall error_message:string, OrError T
-| OK : T -> OrError T.
-Notation "??? T" := (OrError T) (at level 10).
-Implicit Arguments Error [T].
-Implicit Arguments OK [T].
-
-Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
- match oe with
- | Error s => Error s
- | OK t => f t
- end.
-Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
-
-Fixpoint list2vecOrError {T}(l:list T)(n:nat) : ???(vec T n) :=
- match n as N return ???(vec _ N) with
- | O => match l with
- | nil => OK vec_nil
- | _ => Error "list2vecOrError: list was too long"
- end
- | S n' => match l with
- | nil => Error "list2vecOrError: list was too short"
- | t::l' => list2vecOrError l' n' >>= fun l'' => OK (vec_cons t l'')
- end
- end.
-
-Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
-| Indexed_Error : forall error_message:string, Indexed f (Error error_message)
-| Indexed_OK : forall t, f t -> Indexed f (OK t)
-.
-Ltac xauto := try apply Indexed_Error; try apply Indexed_OK.
-
-
-
-
-
-
-(* for a type with decidable equality, we can maintain lists of distinct elements *)
-Section DistinctList.
- Context `{V:EqDecidable}.
-
- Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
- match cvl with
- | nil => cv::nil
- | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
- end.
-
- Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
- match cvl with
- | nil => nil
- | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
- end.
-
- Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
- match cvrem with
- | nil => cvl
- | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
- end.
-
- Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
- match cvl1 with
- | nil => cvl2
- | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
- end.
-End DistinctList.
(* Chapter 2.2: Initial and Terminal Objects *)
(******************************************************************************)
-(* Definition 2.7 *)
-Class Initial
-`( C : Category ) :=
-{ zero : C
+Class InitialObject
+`{ C : Category }
+ ( initial_obj : C ) :=
+{ zero := initial_obj
; bottom : forall a, zero ~> a
; bottom_unique : forall `(f:zero~>a), f ~~ (bottom a)
}.
Notation "? A" := (bottom A) : category_scope.
Notation "0" := zero : category_scope.
+Coercion zero : InitialObject >-> ob.
+Implicit Arguments InitialObject [[Ob][Hom]].
-(* Definition 2.7 *)
-Class Terminal
-`( C : Category ) :=
-{ one : C
+Class TerminalObject
+`{ C : Category }
+ ( terminal_obj : C ) :=
+{ one := terminal_obj
; drop : forall a, a ~> one
; drop_unique : forall `(f:a~>one), f ~~ (drop a)
}.
Notation "! A" := (drop A) : category_scope.
Notation "1" := one : category_scope.
+Coercion one : TerminalObject >-> ob.
+Implicit Arguments TerminalObject [[Ob][Hom]].
-(* Proposition 2.8 *)
-(* FIXME: initial and terminal objects are unique up to iso *)
+(* initial objects are unique up to iso *)
+Lemma initial_unique_up_to_iso `{C:Category}{io1:C}(i1:InitialObject C io1){io2:C}(i2:InitialObject C io2) : io1 ≅ io2.
+ refine {| iso_backward := bottom(InitialObject:=i2) io1 ; iso_forward := bottom(InitialObject:=i1) io2 |}.
+ setoid_rewrite (bottom_unique(InitialObject:=i1)); reflexivity.
+ setoid_rewrite (bottom_unique(InitialObject:=i2)); reflexivity.
+ Qed.
+
+(* terminal objects are unique up to iso *)
+Lemma terminal_unique_up_to_iso `{C:Category}{to1:C}(t1:TerminalObject C to1){to2:C}(t2:TerminalObject C to2) : to1 ≅ to2.
+ refine {| iso_backward := drop(TerminalObject:=t1) to2 ; iso_forward := drop(TerminalObject:=t2) to1 |}.
+ setoid_rewrite (drop_unique(TerminalObject:=t1)); reflexivity.
+ setoid_rewrite (drop_unique(TerminalObject:=t2)); reflexivity.
+ Qed.
Defined.
(* the composition of two isomorphisms is an isomorphism *)
-Definition id_comp `{C:Category}{a b c:C}(i1:Isomorphic a b)(i2:Isomorphic b c) : Isomorphic a c.
+Definition iso_comp `{C:Category}{a b c:C}(i1:Isomorphic a b)(i2:Isomorphic b c) : Isomorphic a c.
intros; apply (@Build_Isomorphic _ _ C a c (#i1 >>> #i2) (#i2⁻¹ >>> #i1⁻¹));
setoid_rewrite juggle3;
[ setoid_rewrite (iso_comp1 i2) | setoid_rewrite (iso_comp2 i1) ];
}.
Class CartesianCat `(mc:MonoidalCat) :=
-{ car_terminal :> Terminal mc
-; car_one : one ≅ pmon_I
+{ car_terminal :> TerminalObject mc pmon_I
; car_diagonal : DiagonalCat mc
-; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell _))
-; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr _))
+; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (drop a ⋉ a) >>> (#(pmon_cancell _))
+; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ drop a) >>> (#(pmon_cancelr _))
; car_mn := mc
}.
Coercion car_diagonal : CartesianCat >-> DiagonalCat.
-Coercion car_terminal : CartesianCat >-> Terminal.
+Coercion car_terminal : CartesianCat >-> TerminalObject.
Coercion car_mn : CartesianCat >-> MonoidalCat.
intros.
destruct N1 as [ ni_iso1 ni_commutes1 ].
destruct N2 as [ ni_iso2 ni_commutes2 ].
- exists (fun A => id_comp (ni_iso1 A) (ni_iso2 A)).
+ exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)).
abstract (intros; simpl;
setoid_rewrite <- associativity;
setoid_rewrite <- ni_commutes1;
Defined.
Definition ni_respects
- `{A:Category}`{B:Category}`{C:Category}
- {F0obj}{F0:Functor A B F0obj}
- {F1obj}{F1:Functor A B F1obj}
- {G0obj}{G0:Functor B C G0obj}
- {G1obj}{G1:Functor B C G1obj}
+ `{A:Category}`{B:Category}
+ {F0obj}(F0:Functor A B F0obj)
+ {F1obj}(F1:Functor A B F1obj)
+ `{C:Category}
+ {G0obj}(G0:Functor B C G0obj)
+ {G1obj}(G1:Functor B C G1obj)
: (F0 <~~~> F1) -> (G0 <~~~> G1) -> ((F0 >>>> G0) <~~~> (F1 >>>> G1)).
intro phi.
intro psi.
destruct psi as [ psi_niso psi_comm ].
destruct phi as [ phi_niso phi_comm ].
refine {| ni_iso :=
- (fun a => id_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))) |}.
+ (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))) |}.
abstract (intros; simpl;
setoid_rewrite <- associativity;
setoid_rewrite fmor_preserves_comp;
intros.
destruct N1 as [ ni_iso1 ni_commutes1 ].
destruct N2 as [ ni_iso2 ni_commutes2 ].
- exists (fun A => id_comp (ni_iso1 A) (ni_iso2 A)).
+ exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)).
abstract (intros; simpl;
setoid_rewrite <- associativity;
setoid_rewrite <- ni_commutes1;
Defined.
Definition if_respects
- `{A:Category}`{B:Category}`{C:Category}
- {F0obj}{F0:Functor A B F0obj}
- {F1obj}{F1:Functor A B F1obj}
- {G0obj}{G0:Functor B C G0obj}
- {G1obj}{G1:Functor B C G1obj}
+ `{A:Category}`{B:Category}
+ {F0obj}(F0:Functor A B F0obj)
+ {F1obj}(F1:Functor A B F1obj)
+ `{C:Category}
+ {G0obj}(G0:Functor B C G0obj)
+ {G1obj}(G1:Functor B C G1obj)
: (F0 ≃ F1) -> (G0 ≃ G1) -> ((F0 >>>> G0) ≃ (F1 >>>> G1)).
intro phi.
intro psi.
destruct psi as [ psi_niso psi_comm ].
destruct phi as [ phi_niso phi_comm ].
- exists (fun a => id_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))).
+ exists (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))).
abstract (intros; simpl;
setoid_rewrite <- associativity;
setoid_rewrite fmor_preserves_comp;
Context
`{C1:Category}`{C2:Category}
`{D1:Category}`{D2:Category}
- {F1Obj}{F1:@Functor _ _ C1 _ _ D1 F1Obj}
- {F2Obj}{F2:@Functor _ _ C2 _ _ D2 F2Obj}
+ {F1Obj}(F1:@Functor _ _ C1 _ _ D1 F1Obj)
+ {F2Obj}(F2:@Functor _ _ C2 _ _ D2 F2Obj)
`{E1:Category}`{E2:Category}
- {G1Obj}{G1:@Functor _ _ D1 _ _ E1 G1Obj}
- {G2Obj}{G2:@Functor _ _ D2 _ _ E2 G2Obj}.
+ {G1Obj}(G1:@Functor _ _ D1 _ _ E1 G1Obj)
+ {G2Obj}(G2:@Functor _ _ D2 _ _ E2 G2Obj).
Definition ni_prod_comp_iso A : (((F1 >>>> G1) **** (F2 >>>> G2)) A) ≅ (((F1 **** F2) >>>> (G1 **** G2)) A).
unfold functor_fobj.
Class PreMonoidalFunctor
`(PM1:PreMonoidalCat(C:=C1)(I:=I1))
`(PM2:PreMonoidalCat(C:=C2)(I:=I2))
- (fobj : C1 -> C2 ) :=
+ (fobj : C1 -> C2 ) :=
{ mf_F :> Functor C1 C2 fobj
; mf_i : I2 ≅ mf_F I1
; mf_first : ∀ a, mf_F >>>> bin_first (mf_F a) <~~~> bin_first a >>>> mf_F
}.
Coercion mf_F : PreMonoidalFunctor >-> Functor.
-Definition PreMonoidalFunctorsCompose
+Section PreMonoidalFunctorsCompose.
+ Context
`{PM1 :PreMonoidalCat(C:=C1)(I:=I1)}
`{PM2 :PreMonoidalCat(C:=C2)(I:=I2)}
{fobj12:C1 -> C2 }
(PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
`{PM3 :PreMonoidalCat(C:=C3)(I:=I3)}
{fobj23:C2 -> C3 }
- (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23)
- : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12).
- admit.
- Defined.
+ (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23).
+
+ Definition compose_mf := PMF12 >>>> PMF23.
+
+ Definition compose_mf_i : I3 ≅ PMF23 (PMF12 I1).
+ eapply iso_comp.
+ apply (mf_i(PreMonoidalFunctor:=PMF23)).
+ apply functors_preserve_isos.
+ apply (mf_i(PreMonoidalFunctor:=PMF12)).
+ Defined.
+
+ Definition compose_mf_first a : compose_mf >>>> bin_first (compose_mf a) <~~~> bin_first a >>>> compose_mf.
+ set (mf_first(PreMonoidalFunctor:=PMF12) a) as mf_first12.
+ set (mf_first(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_first23.
+ unfold functor_fobj in *; simpl in *.
+ unfold compose_mf.
+ eapply ni_comp.
+ apply (ni_associativity PMF12 PMF23 (- ⋉fobj23 (fobj12 a))).
+ eapply ni_comp.
+ apply (ni_respects PMF12 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)).
+ apply ni_id.
+ apply mf_first23.
+ clear mf_first23.
+
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity PMF12 (- ⋉fobj12 a) PMF23).
+
+ apply ni_inv.
+ eapply ni_comp.
+ eapply ni_inv.
+ eapply (ni_associativity _ PMF12 PMF23).
+
+ apply ni_respects; [ idtac | apply ni_id ].
+ apply ni_inv.
+ apply mf_first12.
+ Defined.
+
+ Definition compose_mf_second a : compose_mf >>>> bin_second (compose_mf a) <~~~> bin_second a >>>> compose_mf.
+ set (mf_second(PreMonoidalFunctor:=PMF12) a) as mf_second12.
+ set (mf_second(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_second23.
+ unfold functor_fobj in *; simpl in *.
+ unfold compose_mf.
+ eapply ni_comp.
+ apply (ni_associativity PMF12 PMF23 (fobj23 (fobj12 a) ⋊-)).
+ eapply ni_comp.
+ apply (ni_respects PMF12 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)).
+ apply ni_id.
+ apply mf_second23.
+ clear mf_second23.
+
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity PMF12 (fobj12 a ⋊ -) PMF23).
+
+ apply ni_inv.
+ eapply ni_comp.
+ eapply ni_inv.
+ eapply (ni_associativity (a ⋊-) PMF12 PMF23).
+
+ apply ni_respects; [ idtac | apply ni_id ].
+ apply ni_inv.
+ apply mf_second12.
+ Defined.
+
+ Lemma compose_assoc_coherence a b c :
+ (#((pmon_assoc (compose_mf a) (fobj23 (fobj12 c))) (compose_mf b)) >>>
+ compose_mf a ⋊ #((compose_mf_second b) c)) >>>
+ #((compose_mf_second a) (b ⊗ c)) ~~
+ (#((compose_mf_second a) b) ⋉ fobj23 (fobj12 c) >>>
+ #((compose_mf_second (a ⊗ b)) c)) >>> compose_mf \ #((pmon_assoc a c) b).
+(*
+ set (mf_assoc a b c) as x.
+ set (mf_assoc (fobj12 a) (fobj12 b) (fobj12 c)) as x'.
+ unfold functor_fobj in *.
+ simpl in *.
+ etransitivity.
+ etransitivity.
+ etransitivity.
+ Focus 3.
+ apply x'.
+
+ apply iso_shift_left' in x'.
+
+ unfold compose_mf_second; simpl.
+ unfold functor_fobj; simpl.
+ set (mf_second (fobj12 b)) as m.
+ assert (mf_second (fobj12 b)=m). reflexivity.
+ destruct m; simpl.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+
+ set (mf_second (fobj12 (a ⊗ b))) as m''.
+ assert (mf_second (fobj12 (a ⊗ b))=m''). reflexivity.
+ destruct m''; simpl.
+ unfold functor_fobj; simpl.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+
+ set (mf_second (fobj12 a)) as m'.
+ assert (mf_second (fobj12 a)=m'). reflexivity.
+ destruct m'; simpl.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite left_identity.
+ setoid_rewrite right_identity.
+ assert (fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 (b ⊗ c)) ~~ id _).
+ (* *)
+ setoid_rewrite H2.
+ setoid_rewrite left_identity.
+ assert ((id (fobj23 (fobj12 a) ⊗ fobj23 (fobj12 b)) ⋉ fobj23 (fobj12 c)) ~~ id _).
+ (* *)
+ setoid_rewrite H3.
+ setoid_rewrite left_identity.
+ assert (id (fobj23 (fobj12 a ⊗ fobj12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
+ (* *)
+ setoid_rewrite H4.
+ setoid_rewrite left_identity.
+ clear H4.
+ setoid_rewrite left_identity.
+ assert (id (fobj23 (fobj12 (a ⊗ b))) ⋉ fobj23 (fobj12 c) ~~ id _).
+ (* *)
+ setoid_rewrite H4.
+ setoid_rewrite right_identity.
+ clear H4.
+ assert ((fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
+ (* *)
+ setoid_rewrite H4.
+ setoid_rewrite left_identity.
+ clear H4.
+ unfold functor_comp in ni_commutes0; simpl in ni_commutes0.
+ unfold functor_comp in ni_commutes; simpl in ni_commutes.
+ unfold functor_comp in ni_commutes1; simpl in ni_commutes1.
+
+
+ unfold functor_fobj in *.
+ simpl in *.
+ setoid_rewrite x in x'.
+ rewrite H1.
+ set (ni_commutes0 (a )
+ setoid_rewrite fmor_preserves_id.
+ etransitivity.
+ eapply comp_respects.
+ reflexivity.
+ eapply comp_respects.
+ eapply comp_respects.
+ apply
+ Focus 2.
+ eapply fmor_preserves_id.
+ setoid_rewrite (fmor_preserves_id PMF23).
+*)
+ admit.
+ Qed.
+
+ Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12) :=
+ { mf_i := compose_mf_i
+ ; mf_F := compose_mf
+ ; mf_first := compose_mf_first
+ ; mf_second := compose_mf_second }.
+ intros; unfold compose_mf_first; unfold compose_mf_second.
+ set (mf_first (PMF12 a)) as x in *.
+ set (mf_second (PMF12 b)) as y in *.
+ assert (x=mf_first (PMF12 a)). reflexivity.
+ assert (y=mf_second (PMF12 b)). reflexivity.
+ destruct x.
+ destruct y.
+ simpl.
+ repeat setoid_rewrite left_identity.
+ repeat setoid_rewrite right_identity.
+ set (mf_consistent (PMF12 a) (PMF12 b)) as later.
+ apply comp_respects; try reflexivity.
+ unfold functor_comp.
+ unfold functor_fobj; simpl.
+ set (ni_commutes _ _ (id (fobj12 b))) as x.
+ unfold functor_comp in x.
+ simpl in x.
+ unfold functor_fobj in x.
+ symmetry in x.
+ etransitivity.
+ apply x.
+ clear x.
+ set (ni_commutes0 _ _ (id (fobj12 a))) as x'.
+ unfold functor_comp in x'.
+ simpl in x'.
+ unfold functor_fobj in x'.
+ etransitivity; [ idtac | apply x' ].
+ clear x'.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+ rewrite <- H in later.
+ rewrite <- H0 in later.
+ simpl in later.
+ apply later.
+ apply fmor_respects.
+ apply (mf_consistent a b).
+
+ intros.
+ simpl.
+ apply mf_center.
+ apply mf_center.
+ auto.
+
+ intros.
+ unfold compose_mf_first; simpl.
+ set (mf_first (PMF12 b)) as m.
+ assert (mf_first (PMF12 b)=m). reflexivity.
+ destruct m.
+ simpl.
+ unfold functor_fobj; simpl.
+ repeat setoid_rewrite <- fmor_preserves_comp.
+ repeat setoid_rewrite left_identity.
+ repeat setoid_rewrite right_identity.
+
+ set (mf_cancell b) as y.
+ set (mf_cancell (fobj12 b)) as y'.
+ unfold functor_fobj in *.
+ setoid_rewrite y in y'.
+ clear y.
+ setoid_rewrite <- fmor_preserves_comp in y'.
+ setoid_rewrite <- fmor_preserves_comp in y'.
+ etransitivity.
+ apply y'.
+ clear y'.
+
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+ apply comp_respects; try reflexivity.
+ repeat setoid_rewrite associativity.
+ apply comp_respects; try reflexivity.
+
+ set (ni_commutes _ _ (id (fobj12 I1))) as x.
+ unfold functor_comp in x.
+ unfold functor_fobj in x.
+ simpl in x.
+ setoid_rewrite <- x.
+ clear x.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+
+ rewrite H.
+ simpl.
+ clear H.
+ unfold functor_comp in ni_commutes.
+ simpl in ni_commutes.
+ apply ni_commutes.
+
+ intros.
+ unfold compose_mf_second; simpl.
+ set (mf_second (PMF12 a)) as m.
+ assert (mf_second (PMF12 a)=m). reflexivity.
+ destruct m.
+ simpl.
+ unfold functor_fobj; simpl.
+ repeat setoid_rewrite <- fmor_preserves_comp.
+ repeat setoid_rewrite left_identity.
+ repeat setoid_rewrite right_identity.
+
+ set (mf_cancelr a) as y.
+ set (mf_cancelr (fobj12 a)) as y'.
+ unfold functor_fobj in *.
+ setoid_rewrite y in y'.
+ clear y.
+ setoid_rewrite <- fmor_preserves_comp in y'.
+ setoid_rewrite <- fmor_preserves_comp in y'.
+ etransitivity.
+ apply y'.
+ clear y'.
+
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+ apply comp_respects; try reflexivity.
+ repeat setoid_rewrite associativity.
+ apply comp_respects; try reflexivity.
+
+ set (ni_commutes _ _ (id (fobj12 I1))) as x.
+ unfold functor_comp in x.
+ unfold functor_fobj in x.
+ simpl in x.
+ setoid_rewrite <- x.
+ clear x.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+
+ rewrite H.
+ simpl.
+ clear H.
+ unfold functor_comp in ni_commutes.
+ simpl in ni_commutes.
+ apply ni_commutes.
+
+ apply compose_assoc_coherence.
+ Defined.
+
+End PreMonoidalFunctorsCompose.
+
(*******************************************************************************)
(* Braided and Symmetric Categories *)
}.
-Section PreMonoidalSubCategory.
+(* a wide subcategory inherits the premonoidal structure if it includes all of the coherence maps *)
+Section PreMonoidalWideSubcategory.
+
+ Context `(pm:PreMonoidalCat(I:=pmI)).
+ Context {Pmor}(S:WideSubcategory pm Pmor).
+ Context (Pmor_first : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (f ⋉ c)).
+ Context (Pmor_second : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (c ⋊ f)).
+ Context (Pmor_assoc : forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)).
+ Context (Pmor_unassoc: forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)⁻¹).
+ Context (Pmor_cancell: forall {a}, Pmor _ _ #(pmon_cancell a)).
+ Context (Pmor_uncancell: forall {a}, Pmor _ _ #(pmon_cancell a)⁻¹).
+ Context (Pmor_cancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)).
+ Context (Pmor_uncancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)⁻¹).
+ Implicit Arguments Pmor_first [[a][b][c][f]].
+ Implicit Arguments Pmor_second [[a][b][c][f]].
+
+ Definition PreMonoidalWideSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' x a)~~{S}~~>(bin_obj' y a).
+ unfold hom; simpl; intros.
+ destruct f.
+ simpl in *.
+ exists (bin_first(BinoidalCat:=pm) a \ x0).
+ apply Pmor_first; auto.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' a x)~~{S}~~>(bin_obj' a y).
+ unfold hom; simpl; intros.
+ destruct f.
+ simpl in *.
+ exists (bin_second(BinoidalCat:=pm) a \ x0).
+ apply Pmor_second; auto.
+ Defined.
+
+ Instance PreMonoidalWideSubcategory_first (a:S) : Functor S S (fun x => bin_obj' x a) :=
+ { fmor := fun x y f => PreMonoidalWideSubcategory_first_fmor a f }.
+ unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct f'; simpl in *.
+ apply (fmor_respects (bin_first(BinoidalCat:=pm) a)); auto.
+ unfold PreMonoidalWideSubcategory_first_fmor; intros; simpl in *.
+ apply (fmor_preserves_id (bin_first(BinoidalCat:=pm) a)); auto.
+ unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct g; simpl in *.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=pm) a)); auto.
+ Defined.
+
+ Instance PreMonoidalWideSubcategory_second (a:S) : Functor S S (fun x => bin_obj' a x) :=
+ { fmor := fun x y f => PreMonoidalWideSubcategory_second_fmor a f }.
+ unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct f'; simpl in *.
+ apply (fmor_respects (bin_second(BinoidalCat:=pm) a)); auto.
+ unfold PreMonoidalWideSubcategory_second_fmor; intros; simpl in *.
+ apply (fmor_preserves_id (bin_second(BinoidalCat:=pm) a)); auto.
+ unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct g; simpl in *.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=pm) a)); auto.
+ Defined.
+
+ Instance PreMonoidalWideSubcategory_is_Binoidal : BinoidalCat S bin_obj' :=
+ { bin_first := PreMonoidalWideSubcategory_first
+ ; bin_second := PreMonoidalWideSubcategory_second }.
+
+ Definition PreMonoidalWideSubcategory_assoc_iso
+ : forall a b c, Isomorphic(C:=S) (bin_obj' (bin_obj' a b) c) (bin_obj' a (bin_obj' b c)).
+ intros.
+ refine {| iso_forward := existT _ _ (Pmor_assoc a b c) ; iso_backward := existT _ _ (Pmor_unassoc a b c) |}.
+ simpl; apply iso_comp1.
+ simpl; apply iso_comp2.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_assoc
+ : forall a b,
+ (PreMonoidalWideSubcategory_second a >>>> PreMonoidalWideSubcategory_first b) <~~~>
+ (PreMonoidalWideSubcategory_first b >>>> PreMonoidalWideSubcategory_second a).
+ intros.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (PreMonoidalWideSubcategory_second a >>>>
+ PreMonoidalWideSubcategory_first b) (PreMonoidalWideSubcategory_first b >>>>
+ PreMonoidalWideSubcategory_second a) (fun c => PreMonoidalWideSubcategory_assoc_iso a c b)).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_second_fmor; simpl.
+ destruct f; simpl.
+ set (ni_commutes (pmon_assoc(PreMonoidalCat:=pm) a b) x) as q.
+ apply q.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_assoc_ll
+ : forall a b,
+ PreMonoidalWideSubcategory_second (a⊗b) <~~~>
+ PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a.
+ intros.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
+ (PreMonoidalWideSubcategory_second (a⊗b))
+ (PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a)
+ (fun c => PreMonoidalWideSubcategory_assoc_iso a b c)).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_second_fmor; simpl.
+ destruct f; simpl.
+ set (ni_commutes (pmon_assoc_ll(PreMonoidalCat:=pm) a b) x) as q.
+ unfold functor_comp in q; simpl in q.
+ set (pmon_coherent_l(PreMonoidalCat:=pm)) as q'.
+ setoid_rewrite q' in q.
+ apply q.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_assoc_rr
+ : forall a b,
+ PreMonoidalWideSubcategory_first (a⊗b) <~~~>
+ PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b.
+ intros.
+ apply ni_inv.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
+ (PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b)
+ (PreMonoidalWideSubcategory_first (a⊗b))
+ (fun c => PreMonoidalWideSubcategory_assoc_iso c a b)).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_second_fmor; simpl.
+ destruct f; simpl.
+ set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=pm) a b) x) as q.
+ unfold functor_comp in q; simpl in q.
+ set (pmon_coherent_r(PreMonoidalCat:=pm)) as q'.
+ setoid_rewrite q' in q.
+ apply iso_shift_right' in q.
+ apply iso_shift_left.
+ symmetry.
+ setoid_rewrite iso_inv_inv in q.
+ setoid_rewrite associativity.
+ apply q.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_cancelr_iso : forall a, Isomorphic(C:=S) (bin_obj' a pmI) a.
+ intros.
+ refine {| iso_forward := existT _ _ (Pmor_cancelr a) ; iso_backward := existT _ _ (Pmor_uncancelr a) |}.
+ simpl; apply iso_comp1.
+ simpl; apply iso_comp2.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_cancell_iso : forall a, Isomorphic(C:=S) (bin_obj' pmI a) a.
+ intros.
+ refine {| iso_forward := existT _ _ (Pmor_cancell a) ; iso_backward := existT _ _ (Pmor_uncancell a) |}.
+ simpl; apply iso_comp1.
+ simpl; apply iso_comp2.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_cancelr : PreMonoidalWideSubcategory_first pmI <~~~> functor_id _.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
+ (PreMonoidalWideSubcategory_first pmI) (functor_id _) PreMonoidalWideSubcategory_cancelr_iso).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_first_fmor; simpl.
+ destruct f; simpl.
+ apply (ni_commutes (pmon_cancelr(PreMonoidalCat:=pm)) x).
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_cancell : PreMonoidalWideSubcategory_second pmI <~~~> functor_id _.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
+ (PreMonoidalWideSubcategory_second pmI) (functor_id _) PreMonoidalWideSubcategory_cancell_iso).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_second_fmor; simpl.
+ destruct f; simpl.
+ apply (ni_commutes (pmon_cancell(PreMonoidalCat:=pm)) x).
+ Defined.
+
+ Instance PreMonoidalWideSubcategory_PreMonoidal : PreMonoidalCat PreMonoidalWideSubcategory_is_Binoidal pmI :=
+ { pmon_assoc := PreMonoidalWideSubcategory_assoc
+ ; pmon_assoc_rr := PreMonoidalWideSubcategory_assoc_rr
+ ; pmon_assoc_ll := PreMonoidalWideSubcategory_assoc_ll
+ ; pmon_cancelr := PreMonoidalWideSubcategory_cancelr
+ ; pmon_cancell := PreMonoidalWideSubcategory_cancell
+ }.
+ apply Build_Pentagon.
+ intros; unfold PreMonoidalWideSubcategory_assoc; simpl.
+ set (pmon_pentagon(PreMonoidalCat:=pm) a b c) as q.
+ simpl in q.
+ apply q.
+ apply Build_Triangle.
+ intros; unfold PreMonoidalWideSubcategory_assoc;
+ unfold PreMonoidalWideSubcategory_cancelr; unfold PreMonoidalWideSubcategory_cancell; simpl.
+ set (pmon_triangle(PreMonoidalCat:=pm) a b) as q.
+ simpl in q.
+ apply q.
+ intros.
+
+ set (pmon_triangle(PreMonoidalCat:=pm)) as q.
+ apply q.
+
+ intros; simpl; reflexivity.
+ intros; simpl; reflexivity.
+
+ intros; simpl.
+ apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
+ apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
+ apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
+
+ intros; simpl.
+ apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
+ apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
+ apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
+
+ intros; simpl.
+ apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
+ apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
+ apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
+ Defined.
+
+End PreMonoidalWideSubcategory.
+
+
+(* a full subcategory inherits the premonoidal structure if it includes the unit object and is closed under object-pairing *)
+(*
+Section PreMonoidalFullSubcategory.
Context `(pm:PreMonoidalCat(I:=pmI)).
- Context {Pobj}{Pmor}(S:SubCategory pm Pobj Pmor).
+ Context {Pobj}(S:FullSubcategory pm Pobj).
Context (Pobj_unit:Pobj pmI).
Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
Implicit Arguments Pobj_closed [[a][b]].
- Context (Pmor_first: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
- Pmor _ _ (Pobj_closed pa pc) (Pobj_closed pb pc) (f ⋉ c)).
- Context (Pmor_second: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
- Pmor _ _ (Pobj_closed pc pa) (Pobj_closed pc pb) (c ⋊ f)).
- Context (Pmor_assoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
- Pmor _ _
- (Pobj_closed (Pobj_closed pa pb) pc)
- (Pobj_closed pa (Pobj_closed pb pc))
- #(pmon_assoc a c b)).
- Context (Pmor_unassoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
- Pmor _ _
- (Pobj_closed pa (Pobj_closed pb pc))
- (Pobj_closed (Pobj_closed pa pb) pc)
- #(pmon_assoc a c b)⁻¹).
- Context (Pmor_cancell: forall {a}(pa:Pobj a),
- Pmor _ _ (Pobj_closed Pobj_unit pa) pa
- #(pmon_cancell a)).
- Context (Pmor_uncancell: forall {a}(pa:Pobj a),
- Pmor _ _ pa (Pobj_closed Pobj_unit pa)
- #(pmon_cancell a)⁻¹).
- Context (Pmor_cancelr: forall {a}(pa:Pobj a),
- Pmor _ _ (Pobj_closed pa Pobj_unit) pa
- #(pmon_cancelr a)).
- Context (Pmor_uncancelr: forall {a}(pa:Pobj a),
- Pmor _ _ pa (Pobj_closed pa Pobj_unit)
- #(pmon_cancelr a)⁻¹).
- Implicit Arguments Pmor_first [[a][b][c][f]].
- Implicit Arguments Pmor_second [[a][b][c][f]].
- Definition PreMonoidalSubCategory_bobj (x y:S) :=
+ Definition PreMonoidalFullSubcategory_bobj (x y:S) :=
existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
- Definition PreMonoidalSubCategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
- (PreMonoidalSubCategory_bobj x a)~~{S}~~>(PreMonoidalSubCategory_bobj y a).
+ Definition PreMonoidalFullSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+ (PreMonoidalFullSubcategory_bobj x a)~~{S}~~>(PreMonoidalFullSubcategory_bobj y a).
unfold hom; simpl; intros.
- destruct f.
destruct a as [a apf].
destruct x as [x xpf].
destruct y as [y ypf].
simpl in *.
- exists (x0 ⋉ a).
- apply Pmor_first; auto.
+ apply (f ⋉ a).
Defined.
- Definition PreMonoidalSubCategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
- (PreMonoidalSubCategory_bobj a x)~~{S}~~>(PreMonoidalSubCategory_bobj a y).
+ Definition PreMonoidalFullSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+ (PreMonoidalFullSubcategory_bobj a x)~~{S}~~>(PreMonoidalFullSubcategory_bobj a y).
unfold hom; simpl; intros.
- destruct f.
destruct a as [a apf].
destruct x as [x xpf].
destruct y as [y ypf].
simpl in *.
- exists (a ⋊ x0).
- apply Pmor_second; auto.
+ apply (a ⋊ f).
Defined.
- Instance PreMonoidalSubCategory_first (a:S)
- : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj x a) :=
- { fmor := fun x y f => PreMonoidalSubCategory_first_fmor a f }.
- unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+ Instance PreMonoidalFullSubcategory_first (a:S)
+ : Functor S S (fun x => PreMonoidalFullSubcategory_bobj x a) :=
+ { fmor := fun x y f => PreMonoidalFullSubcategory_first_fmor a f }.
+ unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
apply (fmor_respects (-⋉x)); auto.
- unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; simpl in *.
+ unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; simpl in *.
apply (fmor_preserves_id (-⋉x)); auto.
- unfold PreMonoidalSubCategory_first_fmor; intros;
- destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+ unfold PreMonoidalFullSubcategory_first_fmor; intros;
+ destruct a; destruct a0; destruct b; destruct c; simpl in *.
apply (fmor_preserves_comp (-⋉x)); auto.
Defined.
- Instance PreMonoidalSubCategory_second (a:S)
- : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj a x) :=
- { fmor := fun x y f => PreMonoidalSubCategory_second_fmor a f }.
- unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+ Instance PreMonoidalFullSubcategory_second (a:S)
+ : Functor S S (fun x => PreMonoidalFullSubcategory_bobj a x) :=
+ { fmor := fun x y f => PreMonoidalFullSubcategory_second_fmor a f }.
+ unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
apply (fmor_respects (x⋊-)); auto.
- unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; simpl in *.
+ unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; simpl in *.
apply (fmor_preserves_id (x⋊-)); auto.
- unfold PreMonoidalSubCategory_second_fmor; intros;
- destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+ unfold PreMonoidalFullSubcategory_second_fmor; intros;
+ destruct a; destruct a0; destruct b; destruct c; simpl in *.
apply (fmor_preserves_comp (x⋊-)); auto.
Defined.
- Instance PreMonoidalSubCategory_is_Binoidal : BinoidalCat S PreMonoidalSubCategory_bobj :=
- { bin_first := PreMonoidalSubCategory_first
- ; bin_second := PreMonoidalSubCategory_second }.
+ Instance PreMonoidalFullSubcategory_is_Binoidal : BinoidalCat S PreMonoidalFullSubcategory_bobj :=
+ { bin_first := PreMonoidalFullSubcategory_first
+ ; bin_second := PreMonoidalFullSubcategory_second }.
- Definition PreMonoidalSubCategory_assoc
+ Definition PreMonoidalFullSubcategory_assoc
: forall a b,
- (PreMonoidalSubCategory_second a >>>> PreMonoidalSubCategory_first b) <~~~>
- (PreMonoidalSubCategory_first b >>>> PreMonoidalSubCategory_second a).
- admit.
+ (PreMonoidalFullSubcategory_second a >>>> PreMonoidalFullSubcategory_first b) <~~~>
+ (PreMonoidalFullSubcategory_first b >>>> PreMonoidalFullSubcategory_second a).
Defined.
- Definition PreMonoidalSubCategory_assoc_ll
+ Definition PreMonoidalFullSubcategory_assoc_ll
: forall a b,
- PreMonoidalSubCategory_second (a⊗b) <~~~>
- PreMonoidalSubCategory_second b >>>> PreMonoidalSubCategory_second a.
+ PreMonoidalFullSubcategory_second (a⊗b) <~~~>
+ PreMonoidalFullSubcategory_second b >>>> PreMonoidalFullSubcategory_second a.
intros.
- admit.
Defined.
- Definition PreMonoidalSubCategory_assoc_rr
+ Definition PreMonoidalFullSubcategory_assoc_rr
: forall a b,
- PreMonoidalSubCategory_first (a⊗b) <~~~>
- PreMonoidalSubCategory_first a >>>> PreMonoidalSubCategory_first b.
+ PreMonoidalFullSubcategory_first (a⊗b) <~~~>
+ PreMonoidalFullSubcategory_first a >>>> PreMonoidalFullSubcategory_first b.
intros.
- admit.
Defined.
- Definition PreMonoidalSubCategory_I := existT _ pmI (Pobj_unit).
+ Definition PreMonoidalFullSubcategory_I := existT _ pmI Pobj_unit.
- Definition PreMonoidalSubCategory_cancelr : PreMonoidalSubCategory_first PreMonoidalSubCategory_I <~~~> functor_id _.
- admit.
+ Definition PreMonoidalFullSubcategory_cancelr
+ : PreMonoidalFullSubcategory_first PreMonoidalFullSubcategory_I <~~~> functor_id _.
Defined.
- Definition PreMonoidalSubCategory_cancell : PreMonoidalSubCategory_second PreMonoidalSubCategory_I <~~~> functor_id _.
- admit.
+ Definition PreMonoidalFullSubcategory_cancell
+ : PreMonoidalFullSubcategory_second PreMonoidalFullSubcategory_I <~~~> functor_id _.
Defined.
- Instance PreMonoidalSubCategory_PreMonoidal : PreMonoidalCat PreMonoidalSubCategory_is_Binoidal PreMonoidalSubCategory_I :=
- { pmon_assoc := PreMonoidalSubCategory_assoc
- ; pmon_assoc_rr := PreMonoidalSubCategory_assoc_rr
- ; pmon_assoc_ll := PreMonoidalSubCategory_assoc_ll
- ; pmon_cancelr := PreMonoidalSubCategory_cancelr
- ; pmon_cancell := PreMonoidalSubCategory_cancell
+ Instance PreMonoidalFullSubcategory_PreMonoidal
+ : PreMonoidalCat PreMonoidalFullSubcategory_is_Binoidal PreMonoidalFullSubcategory_I :=
+ { pmon_assoc := PreMonoidalFullSubcategory_assoc
+ ; pmon_assoc_rr := PreMonoidalFullSubcategory_assoc_rr
+ ; pmon_assoc_ll := PreMonoidalFullSubcategory_assoc_ll
+ ; pmon_cancelr := PreMonoidalFullSubcategory_cancelr
+ ; pmon_cancell := PreMonoidalFullSubcategory_cancell
}.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
Defined.
-
-End PreMonoidalSubCategory.
+End PreMonoidalFullSubcategory.
+*)
\ No newline at end of file
Qed.
(* the central morphisms of a category constitute a subcategory *)
-Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
+Definition Center `(bc:BinoidalCat) : WideSubcategory bc (fun _ _ f => CentralMorphism f).
apply Build_SubCategory; intros.
apply Build_CentralMorphism; intros.
abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
apply central_morphisms_compose; auto.
Qed.
-
Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c).
intro cm.
apply Build_CentralMorphism; simpl; intros.
Context `(pm:PreMonoidalCat(I:=pmI)).
- Definition Center_bobj : Center pm -> Center pm -> Center pm.
- apply PreMonoidalSubCategory_bobj.
- intros; auto.
- Defined.
-
- Definition Center_is_Binoidal : BinoidalCat (Center pm) Center_bobj.
- apply PreMonoidalSubCategory_is_Binoidal.
- intros.
- apply first_preserves_centrality; auto.
- intros.
- apply second_preserves_centrality; auto.
+ Definition Center_is_Binoidal : BinoidalCat (Center pm) bin_obj'.
+ apply PreMonoidalWideSubcategory_is_Binoidal.
+ intros; apply first_preserves_centrality; auto.
+ intros; apply second_preserves_centrality; auto.
Defined.
- Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal (exist _ pmI I).
- apply PreMonoidalSubCategory_PreMonoidal.
+ Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal pmI.
+ apply PreMonoidalWideSubcategory_PreMonoidal.
Defined.
Definition Center_is_Monoidal : MonoidalCat Center_is_PreMonoidal.
apply Build_CommutativeCat.
intros.
apply Build_CentralMorphism; unfold hom;
- intros; destruct f; destruct a; destruct c; destruct d; destruct b; destruct g; simpl in *.
- apply centralmor_second.
- apply centralmor_second.
+ intros; destruct f; destruct g; simpl in *.
+ apply (centralmor_second(CentralMorphism:=c1)).
+ apply (centralmor_second(CentralMorphism:=c0)).
Defined.
End Center_is_Monoidal.
+++ /dev/null
-Require Import Coq.Unicode.Utf8.
-Require Import Coq.Classes.RelationClasses.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Setoids.Setoid.
-Require Setoid.
-Require Import Coq.Strings.String.
-Export Coq.Unicode.Utf8.
-Export Coq.Classes.RelationClasses.
-Export Coq.Classes.Morphisms.
-Export Coq.Setoids.Setoid.
-
-Set Printing Width 130. (* Proof General seems to add an extra two columns of overhead *)
-Generalizable All Variables.
-
-(******************************************************************************)
-(* Preamble *)
-(******************************************************************************)
-
-Reserved Notation "a -~- b" (at level 10).
-Reserved Notation "a ** b" (at level 10).
-Reserved Notation "?? x" (at level 1).
-Reserved Notation "a ,, b" (at level 50).
-Reserved Notation "!! f" (at level 3).
-Reserved Notation "!` x" (at level 2).
-Reserved Notation "`! x" (at level 2).
-Reserved Notation "a ~=> b" (at level 70, right associativity).
-Reserved Notation "H ===> C" (at level 100).
-Reserved Notation "f >>=>> g" (at level 45).
-Reserved Notation "a ~~{ C }~~> b" (at level 100).
-Reserved Notation "f <--> g" (at level 20).
-Reserved Notation "! f" (at level 2).
-Reserved Notation "? f" (at level 2).
-Reserved Notation "# f" (at level 2).
-Reserved Notation "f '⁻¹'" (at level 1).
-Reserved Notation "a ≅ b" (at level 70, right associativity).
-Reserved Notation "C 'ᵒᴾ'" (at level 1).
-Reserved Notation "F \ a" (at level 20).
-Reserved Notation "f >>> g" (at level 45).
-Reserved Notation "a ~~ b" (at level 54).
-Reserved Notation "a ~> b" (at level 70, right associativity).
-Reserved Notation "a ≃ b" (at level 70, right associativity).
-Reserved Notation "a ≃≃ b" (at level 70, right associativity).
-Reserved Notation "a ~~> b" (at level 70, right associativity).
-Reserved Notation "F ~~~> G" (at level 70, right associativity).
-Reserved Notation "F <~~~> G" (at level 70, right associativity).
-Reserved Notation "a ⊗ b" (at level 40).
-Reserved Notation "a ⊗⊗ b" (at level 40).
-Reserved Notation "a ⊕ b" (at level 40).
-Reserved Notation "a ⊕⊕ b" (at level 40).
-Reserved Notation "f ⋉ A" (at level 40).
-Reserved Notation "A ⋊ f" (at level 40).
-Reserved Notation "- ⋉ A" (at level 40).
-Reserved Notation "A ⋊ -" (at level 40).
-Reserved Notation "a *** b" (at level 40).
-Reserved Notation "a ;; b" (at level 45).
-Reserved Notation "[# f #]" (at level 2).
-Reserved Notation "a ---> b" (at level 11, right associativity).
-Reserved Notation "a <- b" (at level 100, only parsing).
-Reserved Notation "G |= S" (at level 75).
-Reserved Notation "F -| G" (at level 75).
-Reserved Notation "a :: b" (at level 60, right associativity).
-Reserved Notation "a ++ b" (at level 60, right associativity).
-Reserved Notation "<[ t @]>" (at level 30).
-Reserved Notation "<[ t @ n ]>" (at level 30).
-Reserved Notation "<[ e ]>" (at level 30).
-Reserved Notation "'Λ' x : t :-> e" (at level 9, right associativity, x ident).
-Reserved Notation "R ==> R' " (at level 55, right associativity).
-Reserved Notation "f ○ g" (at level 100).
-Reserved Notation "a ==[ n ]==> b" (at level 20).
-Reserved Notation "a ==[ h | c ]==> b" (at level 20).
-Reserved Notation "H /⋯⋯/ C" (at level 70).
-Reserved Notation "pf1 === pf2" (at level 80).
-Reserved Notation "a |== b @@ c" (at level 100).
-Reserved Notation "f >>>> g" (at level 45).
-Reserved Notation "a >>[ n ]<< b" (at level 100).
-Reserved Notation "f **** g" (at level 40).
-Reserved Notation "C × D" (at level 40).
-Reserved Notation "C ×× D" (at level 45).
-Reserved Notation "C ⁽ºᑭ⁾" (at level 1).
-
-Reserved Notation "'<[' a '|-' t ']>'" (at level 35).
-
-Reserved Notation "Γ '∌' x" (at level 10).
-Reserved Notation "Γ '∌∌' x" (at level 10).
-Reserved Notation "Γ '∋∋' x : a ∼ b" (at level 10, x at level 99).
-Reserved Notation "Γ '∋' x : c" (at level 10, x at level 99).
-
-Reserved Notation "a ⇛ b" (at level 40).
-Reserved Notation "φ₁ →→ φ₂" (at level 11, right associativity).
-Reserved Notation "a '⊢ᴛy' b : c" (at level 20, b at level 99, c at level 80).
-Reserved Notation "a '⊢ᴄᴏ' b : c ∼ d" (at level 20, b at level 99).
-Reserved Notation "Γ '+' x : c" (at level 50, x at level 99).
-Reserved Notation "Γ '++' x : a ∼ b" (at level 50, x at level 99).
-Reserved Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" (at level 11, φ₂ at level 99, right associativity).
-
-Reserved Notation "Γ > past : present '⊢ᴇ' succedent"
- (at level 52, past at level 99, present at level 50, succedent at level 50).
-
-Reserved Notation "'η'".
-Reserved Notation "'ε'".
-Reserved Notation "'★'".
-
-Notation "a +++ b" := (append a b) (at level 100).
-Close Scope nat_scope. (* so I can redefine '1' *)
-
-Delimit Scope arrow_scope with arrow.
-Delimit Scope biarrow_scope with biarrow.
-Delimit Scope garrow_scope with garrow.
-
-Notation "f ○ g" := (fun x => f(g(x))).
-Notation "?? T" := (option T).
-
-(* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *)
-Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100).
-Notation "'Λ' '⟨' x ',' y '⟩' e" := (fun xy => match xy with (a,b) => (fun x y => e) a b end) (at level 100).
-Notation "'Λ' '⟨' x ',' '⟨' y ',' z '⟩' '⟩' e" :=
- (fun xyz => match xyz with (a,bc) => match bc with (b,c) => (fun x y z => e) a b c end end) (at level 100).
-Notation "'Λ' '⟨' '⟨' x ',' y '⟩' ',' z '⟩' e" :=
- (fun xyz => match xyz with (ab,c) => match ab with (a,b) => (fun x y z => e) a b c end end) (at level 100).
-
-Notation "∀ x y z u q , P" := (forall x y z u q , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v a b r s t , P" := (forall x y z u q v a b r s t , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, t ident,
- right associativity)
- : type_scope.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
-(* Any morphism-predicate which is closed under composition and
- * passing to identity morphisms (of either the domain or codomain)
- *
- * We could recycle the "predicate on morphisms" to determine the
- * "predicate on objects", but this causes technical difficulties with
- * Coq *)
-Class SubCategory `(C:Category Ob Hom)(Pobj:Ob->Type)(Pmor:forall a b:Ob, Pobj a -> Pobj b -> (a~>b) ->Type) : Type :=
-{ sc_id_included : forall (a:Ob)(pa:Pobj a), Pmor _ _ pa pa (id a)
-; sc_comp_included : forall (a b c:Ob)(pa:Pobj a)(pb:Pobj b)(pc:Pobj c) f g,
- (Pmor _ _ pa pb f) -> (Pmor _ _ pb pc g) -> (Pmor _ _ pa pc (f>>>g))
+(*
+ * See the README for an explanation of why there is "WideSubcategory"
+ * and "FullSubcategory" but no "Subcategory"
+ *)
+
+(* a full subcategory requires nothing more than a predicate on objects *)
+Class FullSubcategory `(C:Category)(Pobj:C->Type) := { }.
+
+(* the category construction for full subcategories is simpler: *)
+Instance FullSubCategoriesAreCategories `(fsc:@FullSubcategory Ob Hom C Pobj)
+ : Category (sigT Pobj) (fun dom ran => (projT1 dom)~~{C}~~>(projT1 ran)) :=
+{ id := fun t => id (projT1 t)
+; eqv := fun a b f g => eqv _ _ f g
+; comp := fun a b c f g => f >>> g
}.
+ intros; apply Build_Equivalence. unfold Reflexive.
+ intros; reflexivity.
+ unfold Symmetric; intros; simpl; symmetry; auto.
+ unfold Transitive; intros; simpl. transitivity y; auto.
+ intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto.
+ intros; simpl. apply left_identity.
+ intros; simpl. apply right_identity.
+ intros; simpl. apply associativity.
+ Defined.
+Coercion FullSubCategoriesAreCategories : FullSubcategory >-> Category.
(* every category is a subcategory of itself! *)
+(*
Instance IdentitySubCategory `(C:Category Ob Hom) : SubCategory C (fun _ => True) (fun _ _ _ _ _ => True).
intros; apply Build_SubCategory.
intros; auto.
intros; auto.
Defined.
-
-(* a full subcategory requires nothing more than a predicate on objects *)
-Definition FullSubcategory `(C:Category)(Pobj:C->Type) : SubCategory C Pobj (fun _ _ _ _ _ => True).
- apply Build_SubCategory; intros; auto.
+(* the inclusion operation from a subcategory to its host is a functor *)
+Instance InclusionFunctor `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor)
+ : Functor SP C (fun x => projT1 x) :=
+ { fmor := fun dom ran f => projT1 f }.
+ intros. unfold eqv in H. simpl in H. auto.
+ intros. simpl. reflexivity.
+ intros. simpl. reflexivity.
Defined.
+*)
+
+
+(* a wide subcategory includes all objects, so it requires nothing more than a predicate on each hom-set *)
+Class WideSubcategory `(C:Category Ob Hom)(Pmor:forall a b:Ob, (a~>b) ->Type) : Type :=
+{ wsc_id_included : forall (a:Ob), Pmor a a (id a)
+; wsc_comp_included : forall (a b c:Ob) f g, (Pmor a b f) -> (Pmor b c g) -> (Pmor a c (f>>>g))
+}.
-Section SubCategoriesAreCategories.
- (* Any such predicate determines a category *)
- Instance SubCategoriesAreCategories `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor)
- : Category (sigT Pobj) (fun dom ran => sigT (fun f => Pmor (projT1 dom) (projT1 ran) (projT2 dom) (projT2 ran) f)) :=
- { id := fun t => existT (fun f => Pmor _ _ _ _ f) (id (projT1 t)) (sc_id_included _ (projT2 t))
+(* the category construction for full subcategories is simpler: *)
+Instance WideSubCategoriesAreCategories `{C:Category(Ob:=Ob)}{Pmor}(wsc:WideSubcategory C Pmor)
+ : Category Ob (fun x y => sigT (Pmor x y)) :=
+ { id := fun t => existT _ (id t) (@wsc_id_included _ _ _ _ wsc t)
; eqv := fun a b f g => eqv _ _ (projT1 f) (projT1 g)
- ; comp := fun a b c f g => existT (fun f => Pmor _ _ _ _ f) (projT1 f >>> projT1 g)
- (sc_comp_included _ _ _ (projT2 a) (projT2 b) (projT2 c) _ _ (projT2 f) (projT2 g))
+ ; comp := fun a b c f g => existT (Pmor a c) (projT1 f >>> projT1 g)
+ (@wsc_comp_included _ _ _ _ wsc _ _ _ _ _ (projT2 f) (projT2 g))
+
}.
intros; apply Build_Equivalence. unfold Reflexive.
intros; reflexivity.
intros; simpl. apply right_identity.
intros; simpl. apply associativity.
Defined.
-End SubCategoriesAreCategories.
-Coercion SubCategoriesAreCategories : SubCategory >-> Category.
+Coercion WideSubCategoriesAreCategories : WideSubcategory >-> Category.
-(* the inclusion operation from a subcategory to its host is a functor *)
-Instance InclusionFunctor `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor)
- : Functor SP C (fun x => projT1 x) :=
- { fmor := fun dom ran f => projT1 f }.
- intros. unfold eqv in H. simpl in H. auto.
- intros. simpl. reflexivity.
- intros. simpl. reflexivity.
- Defined.
+(* the full image of a functor is a full subcategory *)
+Section FullImage.
-Definition FullImage `(F:Functor(c1:=C)(c2:=D)(fobj:=Fobj)) := FullSubcategory D (fun d => { c:C & (Fobj c)=d }).
+ Context `(F:Functor(c1:=C)(c2:=D)).
-(* any functor may be restricted to its image *)
-Section RestrictToImage.
- Context `(F:Functor(c1:=C)(c2:=D)(fobj:=Fobj)).
- Definition RestrictToImage_fobj : C -> FullImage F.
- intros.
- exists (F X).
- exists X.
- reflexivity.
- Defined.
- Definition RestrictToImage_fmor a b (f:a~>b) : (RestrictToImage_fobj a)~~{FullImage F}~~>(RestrictToImage_fobj b).
- exists (F \ f); auto.
+ Instance FullImage : Category C (fun x y => (F x)~~{D}~~>(F y)) :=
+ { id := fun t => id (F t)
+ ; eqv := fun x y f g => eqv(Category:=D) _ _ f g
+ ; comp := fun x y z f g => comp(Category:=D) _ _ _ f g
+ }.
+ intros; apply Build_Equivalence. unfold Reflexive.
+ intros; reflexivity.
+ unfold Symmetric; intros; simpl; symmetry; auto.
+ unfold Transitive; intros; simpl. transitivity y; auto.
+ intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto.
+ intros; simpl. apply left_identity.
+ intros; simpl. apply right_identity.
+ intros; simpl. apply associativity.
+ Defined.
+
+ Instance FullImage_InclusionFunctor : Functor FullImage D (fun x => F x) :=
+ { fmor := fun x y f => f }.
+ intros; auto.
+ intros; simpl; reflexivity.
+ intros; simpl; reflexivity.
Defined.
- Instance RestrictToImage : Functor C (FullImage F) RestrictToImage_fobj :=
- { fmor := fun a b f => RestrictToImage_fmor a b f }.
+
+ Instance RestrictToImage : Functor C FullImage (fun x => x) :=
+ { fmor := fun a b f => F \ f }.
intros; simpl; apply fmor_respects; auto.
intros; simpl; apply fmor_preserves_id; auto.
intros; simpl; apply fmor_preserves_comp; auto.
Defined.
- Lemma RestrictToImage_splits : F ≃ (RestrictToImage >>>> InclusionFunctor _ _).
- exists (fun A => iso_id (F A)).
- intros; simpl.
- setoid_rewrite left_identity.
- setoid_rewrite right_identity.
- reflexivity.
- Qed.
-End RestrictToImage.
+ Lemma RestrictToImage_splits : F ~~~~ (RestrictToImage >>>> FullImage_InclusionFunctor).
+ unfold EqualFunctors; simpl; intros; apply heq_morphisms_intro.
+ apply fmor_respects.
+ auto.
+ Defined.
+
+End FullImage.
+
+(*
Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor)
{fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=
{ fmor := fun a b f => fmor F f }.
intros. apply (@fmor_preserves_id _ _ _ _ _ _ _ F a).
intros. apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f).
Defined.
+*)
+(*
(* if a functor's range falls within a subcategory, then it is already a functor into that subcategory *)
Section FunctorWithRangeInSubCategory.
Context `(Cat1:Category O1 Hom1).
*)
End Opposite.
End FunctorWithRangeInSubCategory.
+*)
(* Definition 7.1: faithful functors *)
G >>>> F ≃ H >>>> F
-> G ≃ H.
+(*
Section FullFaithfulFunctor_section.
Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)).
Context (F_full:FullFunctor F).
Definition ff_functor_section_fmor {a b:FullImage F} (f:a~~{FullImage F}~~>b)
: (ff_functor_section_fobj a)~~{C1}~~>(ff_functor_section_fobj b).
destruct a as [ a1 [ a2 a3 ] ].
+ destruct b as [ b1 [ b2 b3 ] ].
+ set (@ff_invert _ _ _ _ _ _ _ _ F_full _ _ f) as f'.
+ destruct a as [ a1 [ a2 a3 ] ].
subst.
unfold ff_functor_section_fobj.
simpl.
Instance ff_functor_section_functor : Functor (FullImage F) C1 ff_functor_section_fobj :=
{ fmor := fun a b f => ff_functor_section_fmor f }.
abstract (intros;
- destruct a; destruct b; destruct s; destruct s0; destruct f; destruct f'; simpl in *;
- subst; simpl; set (F_full x1 x2 x3) as ff1; set (F_full x1 x2 x4) as ff2; destruct ff1; destruct ff2;
+ destruct a; destruct b; destruct s; destruct s0; simpl in *;
+ subst; simpl; set (F_full x1 x2 f) as ff1; set (F_full x1 x2 f') as ff2; destruct ff1; destruct ff2;
apply F_faithful;
etransitivity; [ apply e | idtac ];
symmetry;
destruct c as [ c1 [ c2 c3 ] ];
subst;
simpl in *;
- destruct f;
- destruct g;
simpl in *;
apply ff_functor_section_respectful).
Defined.
FullImage F
}~~> existT (fun d : C2, {c : C1 & Fobj c = d})
(Fobj b2) (existT (fun c : C1, Fobj c = Fobj b2) b2 (eq_refl _)))
- : F \ (let (x1, _) := F_full a2 b2 (let (x1, _) := f in x1) in x1) ~~ projT1 f.
- destruct f.
+ : F \ (let (x1, _) := F_full a2 b2 f in x1) ~~ f.
simpl.
- set (F_full a2 b2 x) as qq.
+ set (F_full a2 b2 f) as qq.
destruct qq.
apply e.
Qed.
destruct b as [ b1 [ b2 b3 ] ].
subst.
simpl in *.
- inversion f; subst.
- inversion f'; subst.
simpl in *.
apply heq_morphisms_intro.
simpl.
+ unfold RestrictToImage_fmor; simpl.
etransitivity; [ idtac | apply H ].
clear H.
clear f'.
destruct A as [ a1 [ a2 a3 ] ].
destruct B as [ b1 [ b2 b3 ] ].
simpl.
- destruct f; subst.
- simpl.
+ unfold RestrictToImage_fmor; simpl.
setoid_rewrite left_identity.
setoid_rewrite right_identity.
set (F_full a2 b2 x) as qr.
Opaque ff_functor_section_splits_niso_helper.
End FullFaithfulFunctor_section.
+*)
\ No newline at end of file
projects / coq-categories.git / commitdiff