--- /dev/null
+build/
+build/**
--- /dev/null
+coqc := coqc -noglob
+coqfiles := $(shell find src -name \*.v)
+allfiles := $(coqfiles) $(shell find src -name \*.hs)
+
+default: $(allfiles)
+ make build/Makefile.coq
+ cd build; make OPT=-dont-load-proofs -f Makefile.coq Main.vo
+
+build/Makefile.coq: $(coqfiles)
+ mkdir -p build
+ rm -f build/*.v
+ rm -f build/*.d
+ cd build; ln -s ../src/*.v .
+ cd build; coq_makefile *.v > Makefile.coq
+
+clean:
+ rm -rf build
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import MonoidalCategories_ch7_8.
+
+(*******************************************************************************)
+(* Chapter 9: Adjoints *)
+(*******************************************************************************)
+
+Class Adjunction `{C:Category}`{D:Category}{Fobj}{Gobj}(L:Functor D C Fobj)(R:Functor C D Gobj) :=
+{ adj_counit : functor_id D ~~~> L >>>> R
+; adj_unit : R >>>> L ~~~> functor_id C
+; adj_pf1 : forall (X:C)(Y:D), id (L Y) ~~ (L \ (adj_counit Y)) >>> (adj_unit (L Y))
+; adj_pf2 : forall (X:C)(Y:D), id (R X) ~~ (adj_counit (R X)) >>> (R \ (adj_unit X))
+(* FIXME: use the definition based on whiskering *)
+}.
+Notation "L -| R" := (Adjunction L R).
+Notation "'ε'" := (adj_counit _).
+Notation "'η'" := (adj_unit _).
+
+(* Definition 9.6 "Official" *)
+(*
+Lemma homset_adjunction `(C:ECategory(V:=V))`(D:ECategory(V:=V))(L:Func C D)(R:Func D C)
+ : (L -| R)
+ -> RepresentableFunctorºᑭ _ _ >>>> YonedaBiFunctor D ≃
+ RepresentableFunctorºᑭ _ _ >>>> YonedaBiFunctor C.
+ *)
+ (* adjuncts are unique up to natural iso *)
+ (* adjuncts compose *)
+ (* adjuncts preserve limits *)
+ (* every adjunction determines a monad, vice versa *)
+ (* E-M category *)
+ (* Kleisli category *)
+ (* if C is enriched, then we get an iso of hom-sets *)
+
+
+
+
+(* Example 9.7: exopnentiation is right adjoint to product *)
+
+(* Example 9.8: terminal object selection is right adjoint to the terminal-functor in Cat *)
+
+(* Proposition 9.9: Adjoints are unique up to iso *)
+
+(* Example 9.9: Product is left adjoint to diagonal, and coproduct is right adjoint; generalizes to limits/colimits *)
+
+
+(* Proposition 9.14: RAPL *)
+
+
+
--- /dev/null
+(******************************************************************************)
+(* Chapter 4: Algebras *)
+(* *)
+(* This formalizes for arbitrary algebras what Awodey does for groups in *)
+(* chapter 4 *)
+(******************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+(* very handy *)
+(*
+Fixpoint listOfTypesToType (args:list Type)(ret:Type) : Type :=
+ match args with
+ | nil => ret
+ | a::b => a -> listOfTypesToType b ret
+ end.
+*)
+
+Section Algebras.
+
+Local Notation "a :: b" := (vec_cons a b).
+Local Notation "[]" := (vec_nil).
+Local Notation "[ a ]" := (a::[]).
+
+Structure Signature : Type :=
+{ sig_sort : Type
+; sig_op : Type
+; sig_arity_len : sig_op -> nat
+; sig_result : sig_op -> sig_sort
+; sig_arity : forall op:sig_op, vec sig_sort (sig_arity_len op)
+}.
+
+Section DerivedOperations.
+
+ Context (sig:Signature).
+
+ Structure Algebra : Type :=
+ { alg_carrier : sig_sort sig -> Type
+ (*; alg_op : forall op:sig_op sig, listOfTypesToType (map alg_carrier (sig_arity sig op)) (alg_carrier (sig_result sig op))*)
+ (*FIXME*)
+ }.
+
+ (* the "arity" of an operation in a multi-sorted signature is a finite list of sorts *)
+ Definition Arity := { n:nat & vec (sig_sort sig) n }.
+ Definition mkArity {n:nat} : vec (sig_sort sig) n -> Arity.
+ intros v; exists n; auto.
+ Defined.
+ Definition length : Arity -> nat.
+ intro a; destruct a; auto.
+ Defined.
+
+ Definition arity_get (n:nat)(a:Arity)(pf:lt n (length a)) : sig_sort sig.
+ destruct a.
+ refine (@vec_get (sig_sort sig) _ v n pf).
+ Defined.
+
+ (* See Bergman, Invitation to Universal Algebra, Def 8.9.1 *)
+ Inductive DerivedOperation : Arity -> sig_sort sig -> Type :=
+ | do_op : forall op:sig_op sig, DerivedOperation (mkArity (sig_arity sig op)) (sig_result sig op)
+ | do_projection : forall (a:Arity)(n:nat)(pf:lt n (length a)), DerivedOperation a (arity_get n a pf)
+ | do_compose : forall n a b c, VecOfDerivedOperations n a b -> DerivedOperation (mkArity b) c -> DerivedOperation a c
+ with VecOfDerivedOperations : forall n:nat, Arity -> vec (sig_sort sig) n -> Type :=
+ | vodo_nil : forall a, VecOfDerivedOperations 0 a []
+ | vodo_cons : forall a b n v, DerivedOperation a b -> VecOfDerivedOperations n a v -> VecOfDerivedOperations (S n) a (b::v).
+
+ (* an identity is a pair of derived operations, WLOG having the same arity *)
+ Record Identity :=
+ { id_arity : Arity
+ ; id_result : sig_sort sig
+ ; id_op1 : DerivedOperation id_arity id_result
+ ; id_op2 : DerivedOperation id_arity id_result
+ }.
+
+ Definition Relations := list Identity.
+
+ Inductive Satisfies : Algebra -> Relations -> Prop :=.
+
+End DerivedOperations.
+
+(* TO DO: an algebra of signature [s] in monoidal category [c] *)
+(* FIXME: generators-and-relations *)
+(* see also example 9.36 *)
+
+(*
+An Algebra-Sorted-Signature consists of an algebra of sorts and a
+collection of operations such that each operations's arity is a list
+of elements of the sort algebra.
+*)
+(*
+Structure AlgebraSortedSignature `(relations_on_sort_algebra : Relations signature_of_sort_algebra) : Type :=
+{ algss_sort_algebra : Algebra signature_of_sort_algebra relations_on_sort_algebra
+}.
+
+Structure AlgebraSortedAlgebra {sig}{rel}(algss:@AlgebraSortedSignature sig rel) : Type :=
+{
+}.
+Definition AlgebraSortedSignature_is_Signature : forall sig rel, AlgebraSortedSignature sig rel -> Signature sig rel.
+ Defined.
+ Coercion AlgebraSortedSignature_is_Signature : AlgebraSortedSignature >-> Signature.
+*)
+
+(* algebraically axiomatized monoidal categories *)
+Record AMCat :=
+{ amcat_ob : Type
+; amcat_I : amcat_ob
+; amcat_hom : amcat_ob -> amcat_ob -> Type where "a ~> b" := (amcat_hom a b)
+; amcat_oprod : amcat_ob -> amcat_ob -> amcat_ob where "a ⊗ b" := (amcat_oprod a b)
+
+; amcat_eqv : ∀ a b, a~>b -> a~>b -> Prop where "f ~~ g" := (amcat_eqv _ _ f g)
+; amcat_eqv_eqv : ∀ a b, Equivalence (amcat_eqv a b)
+
+; amcat_id : ∀ a, a~>a
+; amcat_comp : ∀ a b c, a~>b -> b~>c -> a~>c where "f >>> g" := (amcat_comp _ _ _ f g)
+; amcat_mprod : ∀ a b c d, a~>b -> c~>d -> (a⊗c)~>(b⊗d) where "a × b" := (amcat_mprod _ _ _ _ a b)
+ and "f ⋉ A" := (f × (amcat_id A))
+ and "A ⋊ f" := ((amcat_id A) × f)
+
+; amcat_comp_respects : ∀ a b c, Proper (amcat_eqv a b ==> amcat_eqv b c ==> amcat_eqv a c) (amcat_comp _ _ _)
+; amcat_left_identity : forall `(f:a~>b), (amcat_id a >>> f) ~~ f
+; amcat_right_identity : forall `(f:a~>b), f >>> amcat_id b ~~ f
+; amcat_associativity : forall `(f:a~>b)`(g:b~>c)`(h:c~>d), (f >>> g) >>> h ~~ f >>> (g >>> h)
+
+; amcat_mprod_preserves_id : forall a b, (amcat_id a) × (amcat_id b) ~~ (amcat_id (a⊗b))
+; amcat_mprod_preserves_comp : forall `(f1:a1~>b1)`(g1:b1~>c1)`(f2:a2~>b2)`(g2:b2~>c2), (f1>>>g1)×(f2>>>g2) ~~ (f1×f2)>>>(g1×g2)
+
+; amcat_cancell : ∀ a, amcat_I⊗a ~> a
+; amcat_cancelr : ∀ a, a⊗amcat_I ~> a
+; amcat_assoc : ∀ a b c, (a⊗b)⊗c ~> a⊗(b⊗c)
+; amcat_uncancell : ∀ a, a ~> amcat_I⊗a
+; amcat_uncancelr : ∀ a, a ~> a⊗amcat_I
+; amcat_unassoc : ∀ a b c, a⊗(b⊗c) ~> (a⊗b)⊗c
+; amcat_cancell_uncancell : ∀ a, amcat_uncancell a >>> amcat_cancell a ~~ amcat_id a
+; amcat_cancell_uncancelr : ∀ a, amcat_uncancelr a >>> amcat_cancelr a ~~ amcat_id a
+; amcat_assoc_unassoc : ∀ a b c, amcat_unassoc a b c >>> amcat_assoc _ _ _ ~~ amcat_id _
+; amcat_cancell_natural : forall `(f:a~>b), amcat_uncancell _ >>> (amcat_id _ × f) ~~ f >>> amcat_uncancell _
+; amcat_cancelr_natural : forall `(f:a~>b), amcat_uncancelr _ >>> (f × amcat_id _) ~~ f >>> amcat_uncancelr _
+; amcat_assoc_natural : forall `(f:a1~>b1)`(g:a2~>b2)`(h:a3~>b3),
+ amcat_assoc _ _ _ >>> (f × (g × h)) ~~ ((f × g) × h) >>> amcat_assoc _ _ _
+; amcat_pentagon : forall a b c d, amcat_assoc a b c ⋉ d >>> amcat_assoc a _ d >>> a ⋊ amcat_assoc b c d
+ ~~ amcat_assoc _ c d >>> amcat_assoc a b _
+; amcat_triangle : forall a b, amcat_cancelr a ⋉ _ ~~ amcat_assoc _ _ _ >>> _ ⋊ amcat_cancell b
+}.
+
+(* To Do: AMCat is an algebraically-sorted signature *)
+
+(* any given level of the Coq universe hierarchy satisfies the algebraic laws for a monoidal category *)
+Definition Coq_AMCat : AMCat.
+ refine
+ {| amcat_ob := Type
+ ; amcat_I := unit
+ ; amcat_hom := fun a b => a->b
+ ; amcat_oprod := fun a b => prod a b
+ ; amcat_eqv := fun a b f g => forall q, (f q)=(g q)
+ ; amcat_id := fun a x => x
+ ; amcat_comp := fun a b c f g => g ○ f
+ ; amcat_mprod := fun a b c d f g => fun x => let (x1,x2) := x in ((f x1),(g x2))
+ ; amcat_cancell := fun a => fun x => let (x1,x2) := x in x2
+ ; amcat_cancelr := fun a => fun x => let (x1,x2) := x in x1
+ ; amcat_assoc := fun a b c => fun x => let (x12,x3) := x in let (x1,x2) := x12 in (x1,(x2,x3))
+ ; amcat_uncancell := fun a => fun x => (tt,x)
+ ; amcat_uncancelr := fun a => fun x => (x,tt)
+ ; amcat_unassoc := fun a b c => fun x => let (x1,x23) := x in let (x2,x3) := x23 in ((x1,x2),x3)
+ |}; intros; simpl; auto; try destruct q; auto; try destruct p; auto; try destruct p; auto.
+ apply Build_Equivalence; simpl;
+ [ unfold Reflexive; intros; auto
+ | unfold Symmetric; intros; symmetry; auto
+ | unfold Transitive; intros; rewrite H; auto ].
+ unfold Proper; unfold respectful; intros; rewrite H; rewrite H0; reflexivity.
+ Defined.
+ Coercion amcat_ob : AMCat >-> Sortclass.
+
+(* To do: arbitrary algebras internal to an MCat *)
+
+(* hrm, internalization is sort of a (primitive-recursive) operation
+ on signatures –- you take a signature for X and produce the signature
+ of MCats with an internal X *)
+
+Delimit Scope amcat_scope with amcat.
+Open Scope amcat_scope.
+Notation "a ~> b" := (amcat_hom _ a b) : amcat_scope.
+Notation "a ⊗ b" := (amcat_oprod _ a b) : amcat_scope.
+Notation "f ~~ g" := (amcat_eqv _ _ _ f g) : amcat_scope.
+Notation "f >>> g" := (amcat_comp _ _ _ _ f g) : amcat_scope.
+Notation "a × b" := (@amcat_mprod _ _ _ _ _ a b) : amcat_scope.
+Notation "f ⋉ A" := (f × (amcat_id _ A)) : amcat_scope.
+Notation "A ⋊ f" := ((amcat_id _ A) × f) : amcat_scope.
+Notation "'I'" := (amcat_I _) : amcat_scope.
+
+(* what we call a category is actually an AMCat-enriched-Cat *)
+(*
+Record Cat (V:AMCat) :=
+{ cat_ob : Type
+; cat_hom : cat_ob -> cat_ob -> V where "a ⇒ b" := (cat_hom a b)
+; cat_id : ∀ a , I ~> a ⇒ a
+; cat_ecomp : ∀ a b c , (a ⇒ b)⊗(b ⇒ c) ~> (a ⇒ c)
+; cat_left_identity : ∀ a b , cat_id a ⋉ (a ⇒ b) >>> cat_ecomp _ _ _ ~~ amcat_cancell _ _
+; cat_right_identity : ∀ a b , (a ⇒ b) ⋊ cat_id b >>> cat_ecomp _ _ _ ~~ amcat_cancelr _ _
+; cat_associativity : ∀ a b c d, amcat_unassoc _ _ _ (_ ⇒ _) >>> cat_ecomp _ _ _ ⋉ (c ⇒ d) >>> cat_ecomp _ _ _ ~~
+ (a ⇒ b) ⋊ cat_ecomp _ _ _ >>> cat_ecomp _ _ _
+; cat_comp := fun a b c f g => amcat_uncancell V _ >>> (amcat_mprod V I (a⇒ b) I (b⇒ c) f g) >>> cat_ecomp _ _ _
+}.
+
+Close Scope amcat_scope.
+
+Delimit Scope cat_scope with cat.
+Notation "a ~> b" := (cat_hom _ a b) : cat_scope.
+Notation "f ~~ g" := (@amcat_eqv _ _ _ f g) : cat_scope.
+Notation "f >>> g" := (@cat_comp _ _ _ _ _ f g) : cat_scope.
+Close Scope cat_scope.
+
+
+
+
+
+(* a monoidal category enriched in an AMCat *)
+Record MCat (V:AMCat) :=
+{ mcat_cat : Cat V
+(* plus monoidal structure *)
+}.
+(*Notation "a ⊗ b" := (amcat_oprod _ a b) : cat_scope.
+Notation "a × b" := (amcat_mprod _ _ _ _ _ a b) : cat_scope.
+Notation "f ⋉ A" := (f × (amcat_id _ A)) : cat_scope.
+Notation "A ⋊ f" := ((amcat_id A) × f) : cat_scope.
+Notation "'I'" := (amcat_I _) : cat_scope.*)
+
+
+(*
+ * Given an MCat we can derive an AMCat, which can then in turn have
+ * internal stuff –- this is essentially the first externalization
+ * functor (I₀).
+ *)
+(*
+Definition AMCat_from_MCat `(C:MCat V) : AMCat.
+ Defined.
+*)
+
+(* need CategoryWithProducts, then use a category enriched in a category with products to get products of categories *)
+(* it's really only functors we need to change: get rid of the general notion, and allow only EFunctors *)
+(* then we can more easily do functor-categories! *)
+
+*)
+End Algebras.
+
+
--- /dev/null
+(******************************************************************************)
+(* Chapter 1.3: Categories *)
+(******************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+(* definition 1.1 *)
+Class Category
+( Ob : Type )
+( Hom : Ob -> Ob -> Type ) :=
+{ hom := Hom where "a ~> b" := (hom a b)
+; ob := Ob
+
+; id : forall a, a~>a
+; comp : forall a b c, a~>b -> b~>c -> a~>c where "f >>> g" := (comp _ _ _ f g)
+
+; eqv : forall a b, (a~>b) -> (a~>b) -> Prop where "f ~~ g" := (eqv _ _ f g)
+; eqv_equivalence : forall a b, Equivalence (eqv a b)
+; comp_respects : forall a b c, Proper (eqv a b ==> eqv b c ==> eqv a c) (comp _ _ _)
+
+; left_identity : forall `(f:a~>b), id a >>> f ~~ f
+; right_identity : forall `(f:a~>b), f >>> id b ~~ f
+; associativity : forall `(f:a~>b)`(g:b~>c)`(h:c~>d), (f >>> g) >>> h ~~ f >>> (g >>> h)
+}.
+Coercion ob : Category >-> Sortclass.
+
+Notation "a ~> b" := (@hom _ _ _ a b) :category_scope.
+Notation "f ~~ g" := (@eqv _ _ _ _ _ f g) :category_scope.
+Notation "f >>> g" := (comp _ _ _ f g) :category_scope.
+Notation "a ~~{ C }~~> b" := (@hom _ _ C a b) (at level 100) :category_scope.
+ (* curious: I declared a Reserved Notation at the top of the file, but Coq still complains if I remove "at level 100" *)
+
+Open Scope category_scope.
+
+Hint Extern 3 => apply comp_respects.
+Hint Extern 1 => apply left_identity.
+Hint Extern 1 => apply right_identity.
+
+Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:Category Ob Hom)(a b:Ob) : (hom a b) (eqv a b)
+ reflexivity proved by (@Equivalence_Reflexive _ _ (eqv_equivalence a b))
+ symmetry proved by (@Equivalence_Symmetric _ _ (eqv_equivalence a b))
+ transitivity proved by (@Equivalence_Transitive _ _ (eqv_equivalence a b))
+ as parametric_relation_eqv.
+ Add Parametric Morphism `(c:Category Ob Hom)(a b c:Ob) : (comp a b c)
+ with signature (eqv _ _ ==> eqv _ _ ==> eqv _ _) as parametric_morphism_comp.
+ auto.
+ Defined.
+
+Hint Constructors Equivalence.
+Hint Unfold Reflexive.
+Hint Unfold Symmetric.
+Hint Unfold Transitive.
+Hint Extern 1 (Proper _ _) => unfold Proper; auto.
+Hint Extern 1 (Reflexive ?X) => unfold Reflexive; auto.
+Hint Extern 1 (Symmetric ?X) => unfold Symmetric; intros; auto.
+Hint Extern 1 (Transitive ?X) => unfold Transitive; intros; auto.
+Hint Extern 1 (Equivalence ?X) => apply Build_Equivalence.
+Hint Extern 8 (respectful _ _ _ _) => unfold respectful; auto.
+
+Hint Extern 4 (?A ~~ ?A) => reflexivity.
+Hint Extern 6 (?X ~~ ?Y) => apply Equivalence_Symmetric.
+Hint Extern 7 (?X ~~ ?Z) => match goal with [H : ?X ~~ ?Y, H' : ?Y ~~ ?Z |- ?X ~~ ?Z] => transitivity Y end.
+Hint Extern 10 (?X >>> ?Y ~~ ?Z >>> ?Q) => apply comp_respects; auto.
+
+(* handy for rewriting *)
+Lemma juggle1 : forall `{C:Category}`(f:a~>b)`(g:b~>c)`(h:c~>d)`(k:d~>e), (((f>>>g)>>>h)>>>k) ~~ (f>>>(g>>>h)>>>k).
+ intros; setoid_rewrite <- associativity; reflexivity.
+ Defined.
+Lemma juggle2 : forall `{C:Category}`(f:a~>b)`(g:b~>c)`(h:c~>d)`(k:d~>e), (f>>>(g>>>(h>>>k))) ~~ (f>>>(g>>>h)>>>k).
+ intros; repeat setoid_rewrite <- associativity. reflexivity.
+ Defined.
+Lemma juggle3 : forall `{C:Category}`(f:a~>b)`(g:b~>c)`(h:c~>d)`(k:d~>e), ((f>>>g)>>>(h>>>k)) ~~ (f>>>(g>>>h)>>>k).
+ intros; repeat setoid_rewrite <- associativity. reflexivity.
+ Defined.
+
+
+
+
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import InitialTerminal_ch2_2.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import Coherence_ch7_8.
+Require Import MonoidalCategories_ch7_8.
+Require Import Enrichment_ch2_8.
+
+(*******************************************************************************)
+(* Category of Categories enriched in some fixed category V *)
+
+Section CategoryOfCategories.
+
+ Context {VOb}{VHom}(V:Category VOb VHom){VI}{MFobj}{MF}(VM:MonoidalCat V VI MFobj MF).
+
+ Class ECat :=
+ { ecat_obj : Type
+ ; ecat_hom : ecat_obj -> ecat_obj -> VOb
+ ; ecat_cat :> ECategory VM ecat_obj ecat_hom
+ }.
+ Implicit Arguments ecat_obj [ ].
+ Implicit Arguments ecat_cat [ ].
+ Implicit Arguments ecat_hom [ ].
+ Instance ToECat {co}{ch}(c:ECategory VM co ch) : ECat := { ecat_cat := c }.
+
+ Class EFunc (C1 C2:ECat) :=
+ { efunc_fobj : ecat_obj C1 -> ecat_obj C2
+ ; efunc_functor : EFunctor (ecat_cat C1) (ecat_cat C2) efunc_fobj
+ }.
+ Implicit Arguments efunc_fobj [ C1 C2 ].
+ Implicit Arguments efunc_functor [ C1 C2 ].
+ Instance ToEFunc {C1}{C2}{eo}(F:EFunctor (ecat_cat C1) (ecat_cat C2) eo)
+ : EFunc C1 C2 := { efunc_functor := F }.
+
+ (* FIXME: should be enriched in whatever V is enriched in *)
+ Instance CategoryOfCategories : Category ECat EFunc :=
+ { id := fun c => ToEFunc (efunctor_id (ecat_cat c))
+(* ; eqv := fun c1 c2 f1 f2 => f1 ≃ f2 *)
+ ; comp := fun c1 c2 c3 (g:EFunc c1 c2)(f:EFunc c2 c3) => ToEFunc (efunctor_comp _ _ _ (efunc_functor g) (efunc_functor f))
+ }.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+ (* FIXME: show that subcategories are monos in __Cat__ *)
+
+End CategoryOfCategories.
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+(******************************************************************************)
+(* Chapter 3.4: CoEqualizers *)
+(******************************************************************************)
+
+(* FIXME *)
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import NaturalTransformations_ch7_4.
+
+(* these are the coherence diagrams found in Definition 7.23 of Awodey's book *)
+
+(* DO NOT try to inline this into [Pre]MonoidalCat; it triggers a Coq resource consumption bug *)
+
+Section Coherence.
+ Context `{C:Category}
+ {bobj:C->C->C}
+ (first : forall a b c:C, (a~~{C}~~>b) -> ((bobj a c)~~{C}~~>(bobj b c)))
+ (second : forall a b c:C, (a~~{C}~~>b) -> ((bobj c a)~~{C}~~>(bobj c b)))
+ (assoc : forall a b c:C, (bobj (bobj a b) c) ~~{C}~~> (bobj a (bobj b c))).
+
+ Record Pentagon :=
+ { pentagon : forall a b c d, (first _ _ d (assoc a b c )) >>>
+ (assoc a _ d ) >>>
+ (second _ _ a (assoc b c d ))
+ ~~ (assoc _ c d ) >>>
+ (assoc a b _ )
+ }.
+
+ Context {I:C}
+ (cancell : forall a :C, (bobj I a) ~~{C}~~> a)
+ (cancelr : forall a :C, (bobj a I) ~~{C}~~> a).
+
+ Record Triangle :=
+ { triangle : forall a b, (first _ _ b (cancelr a)) ~~ (assoc a I b) >>> (second _ _ a (cancell b))
+
+ (*
+ * This is taken as an axiom in Mac Lane, Categories for the Working
+ * Mathematician, p163, display (8), as well as in Awodey (second
+ * triangle diagram). However, it was shown to be eliminable by
+ * Kelly in Theorem 6 of
+ * http://dx.doi.org/10.1016/0021-8693(64)90018-3 but that was under
+ * different assumptions. To be safe we include it here as an
+ * axiom.
+ *)
+ ; coincide : (cancell I) ~~ (cancelr I)
+ }.
+
+End Coherence.
+
+Coercion pentagon : Pentagon >-> Funclass.
+Coercion triangle : Triangle >-> Funclass.
+
+Implicit Arguments pentagon [ Ob Hom C bobj first second assoc ].
+Implicit Arguments triangle [ Ob Hom C bobj first second assoc I cancell cancelr ].
+Implicit Arguments coincide [ Ob Hom C bobj first second assoc I cancell cancelr ].
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import InitialTerminal_ch2_2.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import Coherence_ch7_8.
+Require Import MonoidalCategories_ch7_8.
+
+(******************************************************************************)
+(* Chapter 2.8: Hom Sets and Enriched Categories *)
+(******************************************************************************)
+
+Class ECategory `(mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI))(Eob:Type)(Ehom:Eob->Eob->V) :=
+{ ehom := Ehom where "a ~~> b" := (ehom a b)
+; eob_eob := Eob
+; e_v := mn
+; eid : forall a, EI~>(a~~>a)
+; eid_central : forall a, CentralMorphism (eid a)
+; ecomp : forall {a b c}, (a~~>b)⊗(b~~>c) ~> (a~~>c)
+; ecomp_central :> forall {a b c}, CentralMorphism (@ecomp a b c)
+; eleft_identity : forall {a b }, eid a ⋉ (a~~>b) >>> ecomp ~~ #(pmon_cancell _ _)
+; eright_identity : forall {a b }, (a~~>b) ⋊ eid b >>> ecomp ~~ #(pmon_cancelr _ _)
+; eassociativity : forall {a b c d}, #(pmon_assoc _ _ _ (_~~>_))⁻¹ >>> ecomp ⋉ (c~~>d) >>> ecomp ~~ (a~~>b) ⋊ ecomp >>> ecomp
+}.
+Notation "a ~~> b" := (@ehom _ _ _ _ _ _ _ _ _ _ a b) : category_scope.
+Coercion eob_eob : ECategory >-> Sortclass.
+
+Lemma ecomp_is_functorial `{ec:ECategory}{a b c}{x}(f:EI~~{V}~~>(a~~>b))(g:EI~~{V}~~>(b~~>c)) :
+ ((x ~~> a) ⋊-) \ (iso_backward ((pmon_cancelr mn) EI) >>> ((- ⋉EI) \ f >>> (((a ~~> b) ⋊-) \ g >>> ecomp))) >>> ecomp ~~
+ ((x ~~> a) ⋊-) \ f >>> (ecomp >>> (#((pmon_cancelr mn) (x ~~> b)) ⁻¹ >>> (((x ~~> b) ⋊-) \ g >>> ecomp))).
+
+ set (@fmor_preserves_comp) as fmor_preserves_comp'.
+
+ (* knock off the leading (x ~~> a) ⋊ f *)
+ repeat setoid_rewrite <- associativity.
+ set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) f) as qq.
+ apply iso_shift_right' in qq.
+ setoid_rewrite <- associativity in qq.
+ apply symmetry in qq.
+ apply iso_shift_left' in qq.
+ apply symmetry in qq.
+ simpl in qq.
+ setoid_rewrite <- qq.
+ clear qq.
+ repeat setoid_rewrite associativity.
+ repeat setoid_rewrite <- fmor_preserves_comp'.
+ repeat setoid_rewrite associativity.
+ apply comp_respects; try reflexivity.
+
+ (* rewrite using the lemma *)
+ assert (forall {a b c x}(g:EI~~{V}~~>(b ~~> c)),
+ ((bin_second(BinoidalCat:=bc) (x ~~> a)) \ ((bin_second(BinoidalCat:=bc) (a ~~> b)) \ g))
+ ~~
+ (#(pmon_assoc mn (x ~~> a) _ _)⁻¹ >>>
+ (bin_second(BinoidalCat:=bc) ((x ~~> a) ⊗ (a ~~> b))) \ g >>> #(pmon_assoc mn (x ~~> a) _ _))).
+ symmetry.
+
+ setoid_rewrite associativity.
+ symmetry.
+ apply iso_shift_right'.
+ setoid_rewrite <- pmon_coherent_l.
+ set (ni_commutes (pmon_assoc_ll (x0~~>a0) (a0~~>b0))) as qq.
+ simpl in *.
+ apply (qq _ _ g0).
+ setoid_rewrite H.
+ clear H.
+
+ (* rewrite using eassociativity *)
+ repeat setoid_rewrite associativity.
+ set (@eassociativity _ _ _ _ _ _ _ _ _ ec x a) as qq.
+ setoid_rewrite <- qq.
+ clear qq.
+ unfold e_v.
+
+ (* knock off the trailing ecomp *)
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+
+ (* cancel out the adjacent assoc/cossa pair *)
+ repeat setoid_rewrite associativity.
+ setoid_rewrite juggle2.
+ etransitivity.
+ apply comp_respects; [ idtac |
+ repeat setoid_rewrite <- associativity;
+ etransitivity; [ idtac | apply left_identity ];
+ apply comp_respects; [ idtac | reflexivity ];
+ apply iso_comp1 ].
+ apply reflexivity.
+
+ (* now swap the order of ecomp⋉(b ~~> c) and ((x ~~> a) ⊗ (a ~~> b))⋊g *)
+ repeat setoid_rewrite associativity.
+ set (@centralmor_first) as se.
+ setoid_rewrite <- se.
+ clear se.
+
+ (* and knock the trailing (x ~~> b)⋊ g off *)
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+
+ (* push the ecomp forward past the rlecnac *)
+ set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (@ecomp _ _ _ _ _ _ _ _ _ ec x a b)) as qq.
+ symmetry in qq.
+ apply iso_shift_left' in qq.
+ setoid_rewrite associativity in qq.
+ symmetry in qq.
+ apply iso_shift_right' in qq.
+ simpl in qq.
+ setoid_rewrite qq.
+ clear qq.
+
+ (* and knock off the trailing ecomp *)
+ apply comp_respects; try reflexivity.
+
+ setoid_replace (iso_backward ((pmon_cancelr mn) ((x ~~> a) ⊗ (a ~~> b)))) with
+ (iso_backward ((pmon_cancelr mn) ((x ~~> a) ⊗ (a ~~> b))) >>> id _).
+ simpl.
+ set (@iso_shift_right') as ibs.
+ simpl in ibs.
+ apply ibs.
+ clear ibs.
+
+ setoid_rewrite (MacLane_ex_VII_1_1 (x~~>a) (a~~>b)).
+ setoid_rewrite juggle3.
+ set (fmor_preserves_comp ((x ~~> a) ⋊-)) as q.
+ simpl in q.
+ setoid_rewrite q.
+ clear q.
+ setoid_rewrite iso_comp1.
+ setoid_rewrite fmor_preserves_id.
+ setoid_rewrite right_identity.
+ apply iso_comp1.
+
+ (* leftovers *)
+ symmetry.
+ apply right_identity.
+ apply ecomp_central.
+ Qed.
+
+Lemma underlying_associativity `{ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)} :
+ forall {a b : Eob} (f : EI ~~{ V }~~> a ~~> b) {c : Eob}
+ (g : EI ~~{ V }~~> b ~~> c) {d : Eob} (h : EI ~~{ V }~~> c ~~> d),
+ ((((#((pmon_cancelr mn) EI) ⁻¹ >>> (f ⋉ EI >>> (a ~~> b) ⋊ g)) >>> ecomp) ⋉ EI >>> (a ~~> c) ⋊ h)) >>> ecomp ~~
+ ((f ⋉ EI >>> (a ~~> b) ⋊ ((#((pmon_cancelr mn) EI) ⁻¹ >>> (g ⋉ EI >>> (b ~~> c) ⋊ h)) >>> ecomp))) >>> ecomp.
+
+ intros; symmetry; etransitivity;
+ [ setoid_rewrite associativity; apply comp_respects;
+ [ apply reflexivity | repeat setoid_rewrite associativity; apply (ecomp_is_functorial(x:=a) g h) ] | idtac ].
+
+ repeat setoid_rewrite <- fmor_preserves_comp.
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+ apply comp_respects; try reflexivity.
+
+ set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) f) as qq.
+ apply iso_shift_right' in qq.
+ symmetry in qq.
+ setoid_rewrite <- associativity in qq.
+ apply iso_shift_left' in qq.
+ apply (fmor_respects (bin_first EI)) in qq.
+ setoid_rewrite <- fmor_preserves_comp in qq.
+ setoid_rewrite qq.
+ clear qq.
+
+ repeat setoid_rewrite <- fmor_preserves_comp.
+ repeat setoid_rewrite associativity.
+ apply comp_respects; try reflexivity.
+
+ repeat setoid_rewrite associativity.
+ set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (@ecomp _ _ _ _ _ _ _ _ _ ec a b c)) as qq.
+ apply iso_shift_right' in qq.
+ symmetry in qq.
+ setoid_rewrite <- associativity in qq.
+ apply iso_shift_left' in qq.
+ symmetry in qq.
+ simpl in qq.
+ setoid_rewrite qq.
+ clear qq.
+
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+
+ idtac.
+ set (iso_shift_left'
+ (iso_backward ((pmon_cancelr mn) (a ~~> b)) ⋉ EI >>> ((a ~~> b) ⋊ g) ⋉ EI) ((a ~~> b) ⋊ g)
+ (((pmon_cancelr mn) ((a ~~> b) ⊗ (b ~~> c))))) as xx.
+ symmetry.
+ etransitivity; [ apply xx | apply comp_respects; try reflexivity ].
+ clear xx.
+
+ setoid_rewrite (fmor_preserves_comp (bin_first EI)).
+ set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) ((iso_backward ((pmon_cancelr mn) (a ~~> b)) >>> (a ~~> b) ⋊ g))) as qq.
+ simpl in qq.
+ setoid_rewrite <- qq.
+ clear qq.
+
+ setoid_rewrite <- associativity.
+ setoid_rewrite iso_comp1.
+ apply left_identity.
+
+ Qed.
+
+Instance Underlying `(ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)) : Category Eob (fun a b => EI~>(a~~>b)) :=
+{ id := fun a => eid a
+; comp := fun a b c g f => #(pmon_cancelr _ _)⁻¹ >>> (g ⋉ _ >>> _ ⋊ f) >>> ecomp
+; eqv := fun a b (f:EI~>(a~~>b))(g:EI~>(a~~>b)) => f ~~ g
+}.
+ abstract (intros; apply Build_Equivalence;
+ [ unfold Reflexive
+ | unfold Symmetric
+ | unfold Transitive]; intros; simpl; auto).
+ abstract (intros; unfold Proper; unfold respectful; intros; simpl;
+ repeat apply comp_respects; try apply reflexivity;
+ [ apply (fmor_respects (bin_first EI)) | idtac ]; auto;
+ apply (fmor_respects (bin_second (a~~>b))); auto).
+ abstract (intros;
+ set (fun c d => centralmor_first(c:=c)(d:=d)(CentralMorphism:=(eid_central a))) as q;
+ setoid_rewrite q;
+ repeat setoid_rewrite associativity;
+ setoid_rewrite eleft_identity;
+ setoid_rewrite <- (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn));
+ setoid_rewrite <- associativity;
+ set (coincide pmon_triangle) as qq;
+ setoid_rewrite qq;
+ simpl;
+ setoid_rewrite iso_comp2;
+ apply left_identity).
+ abstract (intros;
+ repeat setoid_rewrite associativity;
+ setoid_rewrite eright_identity;
+ setoid_rewrite <- (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn));
+ setoid_rewrite <- associativity;
+ simpl;
+ setoid_rewrite iso_comp2;
+ apply left_identity).
+ abstract (intros;
+ repeat setoid_rewrite associativity;
+ apply comp_respects; try reflexivity;
+ repeat setoid_rewrite <- associativity;
+ apply underlying_associativity).
+ Defined.
+Coercion Underlying : ECategory >-> Category.
+
+Class EFunctor
+ `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
+ {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
+ {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
+ (EFobj : Eob1 -> Eob2)
+:=
+{ efunc_fobj := EFobj
+; efunc : forall a b:Eob1, (a ~~> b) ~~{V}~~> ( (EFobj a) ~~> (EFobj b) )
+; efunc_central : forall a b, CentralMorphism (efunc a b)
+; efunc_preserves_id : forall a, eid a >>> efunc a a ~~ eid (EFobj a)
+; efunc_preserves_comp : forall a b c, (efunc a b) ⋉ _ >>> _ ⋊ (efunc b c) >>> ecomp ~~ ecomp >>> efunc a c
+}.
+Coercion efunc_fobj : EFunctor >-> Funclass.
+Implicit Arguments efunc [ Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 EFobj ].
+
+Definition efunctor_id
+ `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
+ {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
+ : EFunctor ec1 ec1 (fun x => x).
+ refine {| efunc := fun a b => id (a ~~> b) |}.
+ abstract (intros; apply Build_CentralMorphism; intros;
+ setoid_rewrite fmor_preserves_id;
+ setoid_rewrite right_identity;
+ setoid_rewrite left_identity;
+ reflexivity).
+ abstract (intros; apply right_identity).
+ abstract (intros;
+ setoid_rewrite fmor_preserves_id;
+ setoid_rewrite right_identity;
+ setoid_rewrite left_identity;
+ reflexivity).
+ Defined.
+
+Definition efunctor_comp
+ `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
+ {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
+ {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
+ {Eob3}{EHom3}(ec3:ECategory mn Eob3 EHom3)
+ {Fobj}(F:EFunctor ec1 ec2 Fobj)
+ {Gobj}(G:EFunctor ec2 ec3 Gobj)
+ : EFunctor ec1 ec3 (Gobj ○ Fobj).
+ refine {| efunc := fun a b => (efunc F a b) >>> (efunc G _ _) |}; intros; simpl.
+ abstract (apply Build_CentralMorphism; intros;
+ [ set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc1
+ ; set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc1
+ ; setoid_rewrite <- (fmor_preserves_comp (-⋉d))
+ ; setoid_rewrite <- (fmor_preserves_comp (-⋉c))
+ ; setoid_rewrite <- associativity
+ ; setoid_rewrite <- fc1
+ ; setoid_rewrite associativity
+ ; setoid_rewrite <- gc1
+ ; reflexivity
+ | set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc2
+ ; set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc2
+ ; setoid_rewrite <- (fmor_preserves_comp (d⋊-))
+ ; setoid_rewrite <- (fmor_preserves_comp (c⋊-))
+ ; setoid_rewrite <- associativity
+ ; setoid_rewrite fc2
+ ; setoid_rewrite associativity
+ ; setoid_rewrite gc2
+ ; reflexivity ]).
+ abstract (setoid_rewrite <- associativity;
+ setoid_rewrite efunc_preserves_id;
+ setoid_rewrite efunc_preserves_id;
+ reflexivity).
+ abstract (repeat setoid_rewrite associativity;
+ set (fmor_preserves_comp (-⋉(b~~>c))) as q; setoid_rewrite <- q; clear q;
+ repeat setoid_rewrite associativity;
+ set (fmor_preserves_comp (((Gobj (Fobj a) ~~> Gobj (Fobj b))⋊-))) as q; setoid_rewrite <- q; clear q;
+ set (fun d e => centralmor_second(c:=d)(d:=e)(CentralMorphism:=(efunc_central(EFunctor:=F) b c))) as qq;
+ setoid_rewrite juggle2;
+ setoid_rewrite juggle2;
+ setoid_rewrite qq;
+ clear qq;
+ repeat setoid_rewrite associativity;
+ set ((efunc_preserves_comp(EFunctor:=G)) (Fobj a) (Fobj b) (Fobj c)) as q;
+ repeat setoid_rewrite associativity;
+ repeat setoid_rewrite associativity in q;
+ setoid_rewrite q;
+ clear q;
+ repeat setoid_rewrite <- associativity;
+ apply comp_respects; try reflexivity;
+ set ((efunc_preserves_comp(EFunctor:=F)) a b c) as q;
+ apply q).
+ Defined.
+
+Instance UnderlyingFunctor `(EF:@EFunctor Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 Eobj)
+ : Functor (Underlying ec1) (Underlying ec2) Eobj :=
+ { fmor := fun a b (f:EI~~{V}~~>(a~~>b)) => f >>> (efunc _ a b) }.
+ abstract (intros; simpl; apply comp_respects; try reflexivity; auto).
+ abstract (intros; simpl; apply efunc_preserves_id).
+ abstract (intros;
+ simpl;
+ repeat setoid_rewrite associativity;
+ setoid_rewrite <- efunc_preserves_comp;
+ repeat setoid_rewrite associativity;
+ apply comp_respects; try reflexivity;
+ set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_first EI)) as qq;
+ setoid_rewrite <- qq;
+ clear qq;
+ repeat setoid_rewrite associativity;
+ apply comp_respects; try reflexivity;
+ repeat setoid_rewrite <- associativity;
+ apply comp_respects; try reflexivity;
+ set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_second (Eobj a ~~> Eobj b))) as qq;
+ setoid_rewrite <- qq;
+ repeat setoid_rewrite <- associativity;
+ apply comp_respects; try reflexivity;
+ clear qq;
+ apply (centralmor_first(CentralMorphism:=(efunc_central a b)))).
+ Defined.
+ Coercion UnderlyingFunctor : EFunctor >-> Functor.
+
+Structure Enrichment :=
+{ enr_v_ob : Type
+; enr_v_hom : enr_v_ob -> enr_v_ob -> Type
+; enr_v : Category enr_v_ob enr_v_hom
+; enr_v_fobj : prod_obj enr_v enr_v -> enr_v_ob
+; enr_v_f : Functor (enr_v ×× enr_v) enr_v enr_v_fobj
+; enr_v_i : enr_v_ob
+; enr_v_mon : MonoidalCat enr_v enr_v_fobj enr_v_f enr_v_i
+; enr_c_obj : Type
+; enr_c_hom : enr_c_obj -> enr_c_obj -> enr_v
+; enr_c : ECategory enr_v_mon enr_c_obj enr_c_hom
+}.
+Coercion enr_c : Enrichment >-> ECategory.
+
+(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
+Structure SurjectiveEnrichment :=
+{ se_enr : Enrichment
+; se_decomp : @treeDecomposition (enr_v se_enr) (option ((enr_c_obj se_enr)*(enr_c_obj se_enr)))
+ (fun t => match t with
+ | None => enr_v_i se_enr
+ | Some x => match x with pair y z => enr_c_hom se_enr y z end
+ end)
+ (fun d1 d2:enr_v se_enr => enr_v_fobj se_enr (pair_obj d1 d2))
+}.
+Coercion se_enr : SurjectiveEnrichment >-> Enrichment.
+
+(* Enriched Fibrations *)
+Section EFibration.
+
+ Context `{E:ECategory}.
+ Context {Eob2}{Ehom2}{B:@ECategory Ob Hom V bin_obj' mn EI mn Eob2 Ehom2}.
+ Context {efobj}(F:EFunctor E B efobj).
+
+ (*
+ * A morphism is prone if its image factors through the image of
+ * another morphism with the same codomain just in case the factor
+ * is the image of a unique morphism. One might say that it
+ * "uniquely reflects factoring through morphisms with the same
+ * codomain".
+ *)
+ Definition Prone {e e'}(φ:EI~~{V}~~>(e'~~>e)) :=
+ forall e'' (ψ:EI~~{V}~~>(e''~~>e)) (g:(efobj e'')~~{B}~~>(efobj e')),
+ (comp(Category:=B) _ _ _ g (φ >>> (efunc F _ _))) ~~
+ ψ >>> (efunc F _ _)
+ -> { χ:e''~~{E}~~>e' & ψ ~~ χ >>> φ & g ~~ comp(Category:=V) _ _ _ χ (efunc F e'' e') }.
+ (* FIXME: χ must also be unique *)
+
+ (* a functor is a Street Fibration if morphisms with codomain in its image are, up to iso, the images of prone morphisms *)
+
+ (* Street was the first to define non-evil fibrations using isomorphisms (for cleavage_pf below) rather than equality *)
+ Structure StreetCleavage (e:E)(b:B)(f:b~~{B}~~>(efobj e)) :=
+ { cleavage_e' : E
+ ; cleavage_pf : (efobj cleavage_e') ≅ b
+ ; cleavage_phi : cleavage_e' ~~{E}~~> e
+ ; cleavage_cart : Prone cleavage_phi
+ ; cleavage_eqv : #cleavage_pf >>> f ~~ comp(Category:=V) _ _ _ cleavage_phi (efunc F _ _)
+ }.
+
+ (* if V, the category enriching E and B is V-enriched, we get a functor Bop->Vint *)
+
+ (* Every equivalence of categories is a Street fibration *)
+
+ (* this is actually a "Street Fibration", the non-evil version of a Grothendieck Fibration *)
+ Definition EFibration := forall e b f, exists cl:StreetCleavage e b f, True.
+
+ Definition ClovenEFibration := forall e b f, StreetCleavage e b f.
+
+ (*
+ * Now, a language has polymorphic types iff its category of
+ * judgments contains a second enriched category, the category of
+ * Kinds, and the category of types is fibered over the category of
+ * Kinds, and the weakening functor-of-fibers has a right adjoint.
+ *
+ * http://ncatlab.org/nlab/show/Grothendieck+fibration
+ *
+ * I suppose we'll need to also ask that the R-functors takes
+ * Prone morphisms to Prone morphisms.
+ *)
+End EFibration.
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+
+(******************************************************************************)
+(* Chapter 2.1: Epic and Monic morphisms *)
+(******************************************************************************)
+
+(* Definition 2.1a *)
+Class Monic `{C:Category}{a b:C}(f:a~>b) : Prop :=
+ monic : forall c (g1 g2:c~>a), g1>>>f ~~ g2>>>f -> g1~~g2.
+Implicit Arguments monic [ C a b Ob Hom ].
+
+(* Definition 2.1b *)
+Class Epic `{C:Category}{a b:C}(f:a~>b) : Prop :=
+ epic : forall c (g1 g2:b~>c), f>>>g1 ~~ f>>>g2 -> g1~~g2.
+Implicit Arguments epic [ C a b Ob Hom ].
+
+(* Proposition 2.6 *)
+Instance iso_epic `(i:Isomorphic) : Epic #i.
+ simpl; unfold Epic; intros.
+ setoid_rewrite <- left_identity.
+ setoid_rewrite <- iso_comp2.
+ setoid_rewrite associativity.
+ setoid_rewrite H; reflexivity.
+ Qed.
+
+(* Proposition 2.6 *)
+Instance iso_monic `(i:Isomorphic) : Monic #i.
+ simpl; unfold Monic; intros.
+ setoid_rewrite <- right_identity.
+ setoid_rewrite <- iso_comp1.
+ setoid_rewrite <- associativity.
+ setoid_rewrite H; reflexivity.
+ Qed.
+
+(* a BiMorphism is an epic monic *)
+Class BiMorphism `{C:Category}{a b:C}(f:a~>b) : Prop :=
+{ bimorphism_epic :> Epic f
+; bimorphism_monic :> Monic f
+}.
+Coercion bimorphism_epic : BiMorphism >-> Epic.
+Coercion bimorphism_monic : BiMorphism >-> Monic.
+
+Class EndoMorphism `{C:Category}(A:C) :=
+ endo : A ~> A.
+
+Class AutoMorphism `{C:Category}(A:C) : Type :=
+{ auto_endo1 : EndoMorphism A
+; auto_endo2 : EndoMorphism A
+; auto_iso : Isomorphism (@endo _ _ _ _ auto_endo1) (@endo _ _ _ _ auto_endo2)
+}.
+
+(*Class Balanced `{C:Category} : Prop :=
+ balanced : forall (a b:C)(f:a~>b), BiMorphism f -> Isomorphism f.*)
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+(******************************************************************************)
+(* Chapter 3.3: Equalizers *)
+(******************************************************************************)
+
+(* FIXME *)
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import ch1_3_Categories.
+Require Import ch1_4_Functors.
+Require Import ch1_5_Isomorphisms.
+
+(*******************************************************************************)
+(* Chapter 7.8: Equivalent Categories *)
+(*******************************************************************************)
+
+(* Definition 7.24 *)
+Class EquivalentCategories `(C:Category)`(D:Category){Fobj}{Gobj}(F:Functor C D Fobj)(G:Functor D C Gobj) :=
+{ ec_forward : F >>>> G ≃ functor_id C
+; ec_backward : G >>>> F ≃ functor_id D
+}.
+
+
+(* FIXME *)
+(* Definition 7.25: TFAE: F is an equivalence of categories, F is full faithful and essentially surjective *)
--- /dev/null
+(*******************************************************************************)
+(* Closed Categories *)
+
+(*Definition ClosedCategory `(C:Category)(CI:C) :=*)
--- /dev/null
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 9.8: Freyd's Adjoint Functor Theorem *)
+(*******************************************************************************)
+
+
+
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+
+(*******************************************************************************)
+(* Chapter 7.5 and 7.7: Functor Categories *)
+(*******************************************************************************)
+
+(* Definition 7.9 *)
+Instance FunctorCategory `(C:Category)`(D:Category)
+ : Category { Fobj : C->D & Functor C D Fobj } (fun F G => (projT2 F) ~~~> (projT2 G)) :=
+{ id := fun F => nt_id (projT2 F)
+; comp := fun F G H nt_f_g nt_g_h => nt_comp nt_f_g nt_g_h
+; eqv := fun F G nt1 nt2 => forall c, (nt1 c) ~~ (nt2 c)
+}.
+ intros.
+ (apply Build_Equivalence;
+ [ unfold Reflexive; unfold respectful; simpl; intros; reflexivity
+ | unfold Symmetric; unfold respectful; simpl; intros; symmetry; auto
+ | unfold Transitive; unfold respectful; simpl; intros; etransitivity; [ apply H | auto ] ]).
+ abstract (intros; unfold Proper; unfold respectful; simpl; intros; setoid_rewrite H0; setoid_rewrite H; reflexivity).
+ abstract (intros; simpl; apply left_identity).
+ abstract (intros; simpl; apply right_identity).
+ abstract (intros; simpl; apply associativity).
+ Defined.
+
+(* functors compose with each other, natural transformations compose with each other -- but you can also
+ * compose a functor with a natural transformation! *)
+Definition LeftWhisker
+ `{C:Category}`{D:Category}`{E:Category}
+ {Fobj}{F:Functor C D Fobj}
+ {Gobj}{G:Functor C D Gobj}
+ (nat:F ~~~> G)
+ {Hobj}(H:Functor D E Hobj) : ((F >>>> H) ~~~> (G >>>> H)).
+ apply Build_NaturalTransformation with (nt_component:=(fun c => H \ (nat c))).
+ abstract (intros;
+ simpl;
+ set (@nt_commutes _ _ _ _ _ _ F _ _ G nat) as nat';
+ setoid_rewrite fmor_preserves_comp;
+ setoid_rewrite <- nat';
+ setoid_rewrite <- (fmor_preserves_comp H);
+ reflexivity).
+ Defined.
+
+Definition RightWhisker
+ `{C:Category}`{D:Category}`{E:Category}
+ {Fobj}(F:Functor C D Fobj)
+ {Gobj}{G:Functor D E Gobj}
+ {Hobj}{H:Functor D E Hobj} : (G ~~~> H) -> ((F >>>> G) ~~~> (F >>>> H)).
+ intro nat.
+ apply Build_NaturalTransformation with (nt_component:=(fun c => (nat (F c)))).
+ abstract (intros;
+ simpl;
+ set (@nt_commutes _ _ _ _ _ _ G _ _ H nat) as nat';
+ setoid_rewrite nat';
+ reflexivity).
+ Defined.
+
+(* also sometimes called "horizontal composition" *)
+Definition GodementMultiplication
+ `{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}
+ : (F0~~~>F1) -> (G0~~~>G1) -> ((F0 >>>> G0)~~~>(F1 >>>> G1)).
+ intro phi.
+ intro psi.
+ apply Build_NaturalTransformation with (nt_component:=(fun (a:A) => G0 \ (phi a) >>> psi (F1 a))).
+ abstract (intros;
+ set (@nt_commutes _ _ _ _ _ _ F0 _ _ F1 phi) as comm1;
+ set (@nt_commutes _ _ _ _ _ _ G0 _ _ G1 psi) as comm2;
+ setoid_rewrite <- comm2;
+ simpl;
+ setoid_rewrite associativity;
+ setoid_rewrite fmor_preserves_comp;
+ setoid_rewrite comm1;
+ setoid_rewrite <- fmor_preserves_comp;
+ repeat setoid_rewrite <- associativity;
+ apply comp_respects; try reflexivity;
+ setoid_rewrite comm2;
+ reflexivity).
+ Defined.
+ (* this operation is also a bifunctor from (FunctorCategory A B)*(FunctorCategory B C) to (FunctorCategory A C);
+ * it is functorial *)
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+
+(******************************************************************************)
+(* Chapter 1.4: Functors *)
+(******************************************************************************)
+
+Class Functor
+`( c1 : Category )
+`( c2 : Category )
+( fobj : c1 -> c2 ) :=
+{ functor_fobj := fobj
+; fmor : forall {a b}, a~>b -> (fobj a)~>(fobj b)
+; fmor_respects : forall a b (f f':a~>b), f~~f' -> fmor f ~~ fmor f'
+; fmor_preserves_id : forall a, fmor (id a) ~~ id (fobj a)
+; fmor_preserves_comp : forall `(f:a~>b)`(g:b~>c), (fmor f) >>> (fmor g) ~~ fmor (f >>> g)
+}.
+ (* register "fmor" so we can rewrite through it *)
+ Implicit Arguments fmor [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
+ Implicit Arguments fmor_respects [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
+ Implicit Arguments fmor_preserves_id [ Ob Hom Ob0 Hom0 c1 c2 fobj ].
+ Implicit Arguments fmor_preserves_comp [ Ob Hom Ob0 Hom0 c1 c2 fobj a b c ].
+ Notation "F \ f" := (fmor F f) : category_scope.
+ Add Parametric Morphism `(C1:Category)`(C2:Category)
+ (Fobj:C1->C2)
+ (F:Functor C1 C2 Fobj)
+ (a b:C1)
+ : (@fmor _ _ C1 _ _ C2 Fobj F a b)
+ with signature ((@eqv C1 _ C1 a b) ==> (@eqv C2 _ C2 (Fobj a) (Fobj b))) as parametric_morphism_fmor'.
+ intros; apply (@fmor_respects _ _ C1 _ _ C2 Fobj F a b x y); auto.
+ Defined.
+ Coercion functor_fobj : Functor >-> Funclass.
+
+(* the identity functor *)
+Definition functor_id `(C:Category) : Functor C C (fun x => x).
+ intros; apply (Build_Functor _ _ C _ _ C (fun x => x) (fun a b f => f)); intros; auto; reflexivity.
+ Defined.
+
+(* the constant functor *)
+Definition functor_const `(C:Category) `{D:Category} (d:D) : Functor C D (fun _ => d).
+ apply Build_Functor with (fmor := fun _ _ _ => id d).
+ intros; reflexivity.
+ intros; reflexivity.
+ intros; auto.
+ Defined.
+
+(* functors compose *)
+Definition functor_comp
+ `(C1:Category)
+ `(C2:Category)
+ `(C3:Category)
+ `(F:@Functor _ _ C1 _ _ C2 Fobj)`(G:@Functor _ _ C2 _ _ C3 Gobj) : Functor C1 C3 (Gobj ○ Fobj).
+ intros. apply (Build_Functor _ _ _ _ _ _ _ (fun a b m => G\(F\m)));
+ [ abstract (intros; setoid_rewrite H ; auto; reflexivity)
+ | abstract (intros; repeat setoid_rewrite fmor_preserves_id; auto; reflexivity)
+ | abstract (intros; repeat setoid_rewrite fmor_preserves_comp; auto; reflexivity)
+ ].
+ Defined.
+Notation "f >>>> g" := (@functor_comp _ _ _ _ _ _ _ _ _ _ f _ g) : category_scope.
+
+
+
+(* this is like JMEq, but for the particular case of ~~; note it does not require any axioms! *)
+Inductive heq_morphisms `{c:Category}{a b:c}(f:a~>b) : forall {a' b':c}, a'~>b' -> Prop :=
+ | heq_morphisms_intro : forall {f':a~>b}, eqv _ _ f f' -> @heq_morphisms _ _ c a b f a b f'.
+Definition heq_morphisms_refl : forall `{c:Category} a b f, @heq_morphisms _ _ c a b f a b f.
+ intros; apply heq_morphisms_intro; reflexivity.
+ Qed.
+Definition heq_morphisms_symm : forall `{c:Category} a b f a' b' f', @heq_morphisms _ _ c a b f a' b' f' -> @heq_morphisms _ _ c a' b' f' a b f.
+ refine(fun ob hom c a b f a' b' f' isd =>
+ match isd with
+ | heq_morphisms_intro f''' z => @heq_morphisms_intro _ _ c _ _ f''' f _
+ end); symmetry; auto.
+ Qed.
+Definition heq_morphisms_tran : forall `{C:Category} a b f a' b' f' a'' b'' f'',
+ @heq_morphisms _ _ C a b f a' b' f' ->
+ @heq_morphisms _ _ C a' b' f' a'' b'' f'' ->
+ @heq_morphisms _ _ C a b f a'' b'' f''.
+ destruct 1.
+ destruct 1.
+ apply heq_morphisms_intro.
+ setoid_rewrite <- H0.
+ apply H.
+ Qed.
+
+(*
+Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:Category Ob Hom)(a b:Ob) : (hom a b) (eqv a b)
+ reflexivity proved by heq_morphisms_refl
+ symmetry proved by heq_morphisms_symm
+ transitivity proved by heq_morphisms_tran
+ as parametric_relation_heq_morphisms.
+ Add Parametric Morphism `(c:Category Ob Hom)(a b c:Ob) : (comp a b c)
+ with signature (eqv _ _ ==> eqv _ _ ==> eqv _ _) as parametric_morphism_comp.
+ auto.
+ Defined.
+*)
+Implicit Arguments heq_morphisms [Ob Hom c a b a' b'].
+Hint Constructors heq_morphisms.
+
+Definition EqualFunctors `{C1:Category}`{C2:Category}{F1obj}(F1:Functor C1 C2 F1obj){F2obj}(F2:Functor C1 C2 F2obj) :=
+ forall a b (f f':a~~{C1}~~>b), f~~f' -> heq_morphisms (F1 \ f) (F2 \ f').
+Notation "f ~~~~ g" := (EqualFunctors f g) (at level 45).
+
+(*
+Class IsomorphicCategories `(C:Category)`(D:Category){Fobj}{Gobj}(F:Functor C D Fobj)(G:Functor D C Gobj) :=
+{ ic_forward : F >>>> G ~~~~ functor_id C
+; ic_backward : G >>>> F ~~~~ functor_id D
+}.
+*)
+
+(* this causes Coq to die: *)
+(* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *)
--- /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.
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+
+(******************************************************************************)
+(* Chapter 2.2: Initial and Terminal Objects *)
+(******************************************************************************)
+
+(* Definition 2.7 *)
+Class Initial
+`( C : Category ) :=
+{ zero : C
+; 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.
+
+(* Definition 2.7 *)
+Class Terminal
+`( C : Category ) :=
+{ one : C
+; 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.
+
+
+(* Proposition 2.8 *)
+(* FIXME: initial and terminal objects are unique up to iso *)
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+
+(******************************************************************************)
+(* Chapter 1.5: Isomorphisms *)
+(******************************************************************************)
+
+Class Isomorphism `{C:Category}{a b:C}(f:a~>b)(g:b~>a) : Prop :=
+{ iso_cmp1 : f >>> g ~~ id a
+; iso_cmp2 : g >>> f ~~ id b
+}.
+(* TO DO: show isos are unique when they exist *)
+
+Class Isomorphic
+`{ C : Category }
+( a b : C ) :=
+{ iso_forward : a~>b
+; iso_backward : b~>a
+; iso_comp1 : iso_forward >>> iso_backward ~~ id a
+; iso_comp2 : iso_backward >>> iso_forward ~~ id b
+(* TO DO: merge this with Isomorphism *)
+}.
+Implicit Arguments iso_forward [ C a b Ob Hom ].
+Implicit Arguments iso_backward [ C a b Ob Hom ].
+Implicit Arguments iso_comp1 [ C a b Ob Hom ].
+Implicit Arguments iso_comp2 [ C a b Ob Hom ].
+Notation "a ≅ b" := (Isomorphic a b) : isomorphism_scope.
+(* the sharp symbol "casts" an isomorphism to the morphism in the forward direction *)
+Notation "# f" := (@iso_forward _ _ _ _ _ f) : isomorphism_scope.
+Open Scope isomorphism_scope.
+
+(* the inverse of an isomorphism is an isomorphism *)
+Definition iso_inv `{C:Category}(a b:C)(is:Isomorphic a b) : Isomorphic b a.
+ intros; apply (Build_Isomorphic _ _ _ _ _ (iso_backward _) (iso_forward _));
+ [ apply iso_comp2 | apply iso_comp1 ].
+ Defined.
+Notation "f '⁻¹'" := (@iso_inv _ _ _ _ _ f) : isomorphism_scope.
+
+(* identity maps are isomorphisms *)
+Definition iso_id `{C:Category}(A:C) : Isomorphic A A.
+ intros; apply (Build_Isomorphic _ _ C A A (id A) (id A)); auto.
+ 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.
+ intros; apply (@Build_Isomorphic _ _ C a c (#i1 >>> #i2) (#i2⁻¹ >>> #i1⁻¹));
+ setoid_rewrite juggle3;
+ [ setoid_rewrite (iso_comp1 i2) | setoid_rewrite (iso_comp2 i1) ];
+ setoid_rewrite right_identity;
+ [ setoid_rewrite (iso_comp1 i1) | setoid_rewrite (iso_comp2 i2) ];
+ reflexivity.
+ Defined.
+
+Definition functors_preserve_isos `{C1:Category}`{C2:Category}{Fo}(F:Functor C1 C2 Fo){a b:C1}(i:Isomorphic a b)
+ : Isomorphic (F a) (F b).
+ refine {| iso_forward := F \ (iso_forward i)
+ ; iso_backward := F \ (iso_backward i)
+ |}.
+ setoid_rewrite fmor_preserves_comp.
+ setoid_rewrite iso_comp1.
+ apply fmor_preserves_id.
+ setoid_rewrite fmor_preserves_comp.
+ setoid_rewrite iso_comp2.
+ apply fmor_preserves_id.
+ Defined.
+
+Lemma iso_shift_right `{C:Category} : forall {a b c:C}(f:b~>c)(g:a~>c)(i:Isomorphic b a), #i⁻¹ >>> f ~~ g -> f ~~ #i >>> g.
+ intros.
+ setoid_rewrite <- H.
+ setoid_rewrite <- associativity.
+ setoid_rewrite iso_comp1.
+ symmetry.
+ apply left_identity.
+ Qed.
+
+Lemma iso_shift_right' `{C:Category} : forall {a b c:C}(f:b~>c)(g:a~>c)(i:Isomorphic a b), #i >>> f ~~ g -> f ~~ #i⁻¹ >>> g.
+ intros.
+ setoid_rewrite <- H.
+ setoid_rewrite <- associativity.
+ setoid_rewrite iso_comp1.
+ symmetry.
+ apply left_identity.
+ Qed.
+
+Lemma iso_shift_left `{C:Category} : forall {a b c:C}(f:a~>b)(g:a~>c)(i:Isomorphic c b), f >>> #i⁻¹ ~~ g -> f ~~ g >>> #i.
+ intros.
+ setoid_rewrite <- H.
+ setoid_rewrite associativity.
+ setoid_rewrite iso_comp1.
+ symmetry.
+ apply right_identity.
+ Qed.
+
+Lemma iso_shift_left' `{C:Category} : forall {a b c:C}(f:a~>b)(g:a~>c)(i:Isomorphic b c), f >>> #i ~~ g -> f ~~ g >>> #i⁻¹.
+ intros.
+ setoid_rewrite <- H.
+ setoid_rewrite associativity.
+ setoid_rewrite iso_comp1.
+ symmetry.
+ apply right_identity.
+ Qed.
--- /dev/null
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 9.6: Kan Extensions *)
+(*******************************************************************************)
--- /dev/null
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 9.7: Locally Cartesian Closed Categories *)
+(*******************************************************************************)
+
+
+
+(* Proposition 9.20: TFAE for categories with a terminal object: it is LCCC, every slice is CCC *)
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+Require Import SliceCategories_ch1_6_4.
+
+Require Import EpicMonic_ch2_1.
+Require Import InitialTerminal_ch2_2.
+Require Import SectionRetract_ch2_4.
+
+Require Import Equalizers_ch3_3.
+Require Import CoEqualizers_ch3_4.
+
+Require Import Algebras_ch4.
+
+Require Import Enrichment_ch2_8.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import FunctorCategories_ch7_7.
+Require Import Coherence_ch7_8.
+Require Import MonoidalCategories_ch7_8.
+
+Require Import Exponentials_ch6.
+Require Import CategoryOfCategories_ch7_1.
+Require Import Yoneda_ch8.
+Require Import Adjoints_ch9.
+
+(*Require Import PolynomialCategories.*)
+(*Require Import CoqCategory.*)
+(*Require Import NaturalDeduction.*)
+(*Require Import NaturalDeductionCategories.*)
+(*Require Import CartesianEnrichmentsHaveMonoidalRepresentableFunctors.*)
+(*Require Import Reification.*)
+(*Require Import GeneralizedArrow.*)
+(*Require Import ReificationFromGArrow.*)
+(*Require Import GArrowFromReification.*)
+(*Require Import Roundtrip.*)
+(*Require Import RoundtripSlides.*)
+
+(* very slow! *)
+(*Require Import FreydCategories.*)
+(*Require Import Arrows.*)
--- /dev/null
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 10: Monads *)
+(*******************************************************************************)
+
+
+
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import InitialTerminal_ch2_2.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import Coherence_ch7_8.
+
+(******************************************************************************)
+(* Chapter 7.8: (Pre)Monoidal Categories *)
+(******************************************************************************)
+
+Class BinoidalCat
+`( C : Category )
+( bin_obj' : C -> C -> C ) :=
+{ bin_obj := bin_obj' where "a ⊗ b" := (bin_obj a b)
+; bin_first : forall a:C, Functor C C (fun x => x⊗a)
+; bin_second : forall a:C, Functor C C (fun x => a⊗x)
+; bin_c := C
+}.
+Coercion bin_c : BinoidalCat >-> Category.
+Notation "a ⊗ b" := (@bin_obj _ _ _ _ _ a b) : category_scope.
+Notation "C ⋊ f" := (@fmor _ _ _ _ _ _ _ (@bin_second _ _ _ _ _ C) _ _ f) : category_scope.
+Notation "g ⋉ C" := (@fmor _ _ _ _ _ _ _ (@bin_first _ _ _ _ _ C) _ _ g) : category_scope.
+Notation "C ⋊ -" := (@bin_second _ _ _ _ _ C) : category_scope.
+Notation "- ⋉ C" := (@bin_first _ _ _ _ _ C) : category_scope.
+
+Class CentralMorphism `{BinoidalCat}`(f:a~>b) : Prop :=
+{ centralmor_first : forall `(g:c~>d), (f ⋉ _ >>> _ ⋊ g) ~~ (_ ⋊ g >>> f ⋉ _)
+; centralmor_second : forall `(g:c~>d), (g ⋉ _ >>> _ ⋊ f) ~~ (_ ⋊ f >>> g ⋉ _)
+}.
+
+(* the central morphisms of a category constitute a subcategory *)
+Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
+ apply Build_SubCategory; intros; apply Build_CentralMorphism; intros.
+ abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
+ setoid_rewrite (fmor_preserves_id(bin_first d));
+ setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+ abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
+ setoid_rewrite (fmor_preserves_id(bin_second d));
+ setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+ abstract (setoid_rewrite <- (fmor_preserves_comp(bin_first c0));
+ setoid_rewrite associativity;
+ setoid_rewrite centralmor_first;
+ setoid_rewrite <- associativity;
+ setoid_rewrite centralmor_first;
+ setoid_rewrite associativity;
+ setoid_rewrite <- (fmor_preserves_comp(bin_first d));
+ reflexivity).
+ abstract (setoid_rewrite <- (fmor_preserves_comp(bin_second d));
+ setoid_rewrite <- associativity;
+ setoid_rewrite centralmor_second;
+ setoid_rewrite associativity;
+ setoid_rewrite centralmor_second;
+ setoid_rewrite <- associativity;
+ setoid_rewrite <- (fmor_preserves_comp(bin_second c0));
+ reflexivity).
+ Qed.
+
+Class CommutativeCat `(BinoidalCat) :=
+{ commutative_central : forall `(f:a~>b), CentralMorphism f
+; commutative_morprod := fun `(f:a~>b)`(g:a~>b) => f ⋉ _ >>> _ ⋊ g
+}.
+Notation "f × g" := (commutative_morprod f g).
+
+Section BinoidalCat_from_Bifunctor.
+ Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
+ Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
+ apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
+ @fmor _ _ _ _ _ _ _ F (pair_obj a0 a) (pair_obj b a) (pair_mor (pair_obj a0 a) (pair_obj b a) f (id a)))); intros; simpl;
+ [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
+ | abstract (set (fmor_preserves_id(F)) as q; apply q)
+ | abstract (etransitivity;
+ [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
+ | set (fmor_respects(F)) as q; apply q ];
+ split; simpl; auto) ].
+ Defined.
+ Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
+ apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
+ @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
+ [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
+ | abstract (set (fmor_preserves_id(F)) as q; apply q)
+ | abstract (etransitivity;
+ [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
+ | set (fmor_respects(F)) as q; apply q ];
+ split; simpl; auto) ].
+ Defined.
+
+ Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
+ refine {| bin_first := BinoidalCat_from_Bifunctor_first
+ ; bin_second := BinoidalCat_from_Bifunctor_second
+ |}.
+ Defined.
+
+ (*
+ Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat (BinoidalCat_from_Bifunctor F).
+ abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
+ etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
+ etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
+ apply (fmor_respects(F));
+ split;
+ [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
+ | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
+ Defined.
+ *)
+End BinoidalCat_from_Bifunctor.
+
+(* not in Awodey *)
+Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
+{ pmon_I := I
+; pmon_bin := bc
+; pmon_cat := C
+; pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
+; pmon_cancelr : (bin_first I) <~~~> functor_id C
+; pmon_cancell : (bin_second I) <~~~> functor_id C
+; pmon_pentagon : Pentagon (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
+; pmon_triangle : Triangle (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
+ (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
+; pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b)
+; pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
+; pmon_coherent_r : forall a c d:C, #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
+; pmon_coherent_l : forall a c d:C, #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
+}.
+(*
+ * Premonoidal categories actually have three associators (the "f"
+ * indicates the position in which the operation is natural:
+ *
+ * assoc : (A ⋊ f) ⋉ C <-> A ⋊ (f ⋉ C)
+ * assoc_rr : (f ⋉ B) ⋉ C <-> f ⋉ (B ⊗ C)
+ * assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗ B) ⋊ f
+ *
+ * Fortunately, in a monoidal category these are all the same natural
+ * isomorphism (and in any case -- monoidal or not -- the objects in
+ * the left column are all the same and the objects in the right
+ * column are all the same). This formalization assumes that is the
+ * case even for premonoidal categories with non-central maps, in
+ * order to keep the complexity manageable. I don't know much about
+ * the consequences of having them and letting them be different; you
+ * might need extra versions of the triangle/pentagon diagrams.
+ *)
+
+Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I ].
+Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I ].
+Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I ].
+Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
+
+(* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
+Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
+ : #((pmon_cancelr mn) (a ⊗ b)) ~~ #((pmon_assoc mn a EI) b) >>> (a ⋊-) \ #((pmon_cancelr mn) b).
+ set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
+ set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
+ apply (fmor_respects(bin_second EI)) in tria.
+ set (@fmor_preserves_comp) as fpc.
+ setoid_rewrite <- fpc in tria.
+ set (ni_commutes (pmon_assoc mn a b)) as xx.
+ (* FIXME *)
+ Admitted.
+
+(* Formalized Definition 3.10 *)
+Class PreMonoidalFunctor
+`(PM1:PreMonoidalCat(C:=C1)(I:=I1))
+`(PM2:PreMonoidalCat(C:=C2)(I:=I2))
+ (fobj : C1 -> C2 ) :=
+{ mf_F :> Functor C1 C2 fobj
+; mf_preserves_i : mf_F I1 ≅ I2
+; mf_preserves_first : forall a, bin_first a >>>> mf_F <~~~> mf_F >>>> bin_first (mf_F a)
+; mf_preserves_second : forall a, bin_second a >>>> mf_F <~~~> mf_F >>>> bin_second (mf_F a)
+; mf_preserves_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
+}.
+Coercion mf_F : PreMonoidalFunctor >-> Functor.
+
+(*******************************************************************************)
+(* Braided and Symmetric Categories *)
+
+Class BraidedCat `(mc:PreMonoidalCat) :=
+{ br_swap : forall a b, a⊗b ≅ b⊗a
+; triangleb : forall a:C, #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
+; hexagon1 : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
+ ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
+; hexagon2 : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
+ ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
+}.
+
+Class SymmetricCat `(bc:BraidedCat) :=
+{ symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
+}.
+
+Class DiagonalCat `(BinoidalCat) :=
+{ copy : forall a, a ~> (a⊗a)
+(* copy >> swap == copy -- only necessary for non-cartesian braided diagonal categories *)
+}.
+
+Class CartesianCat `(mc:PreMonoidalCat(C:=C)) :=
+{ car_terminal : Terminal C
+; car_one : 1 ≅ pmon_I
+; car_diagonal : DiagonalCat mc
+; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) _) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
+; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) _) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
+; car_cat := C
+; car_mn := mc
+}.
+Coercion car_diagonal : CartesianCat >-> DiagonalCat.
+Coercion car_terminal : CartesianCat >-> Terminal.
+Coercion car_mn : CartesianCat >-> PreMonoidalCat.
+
+(* Definition 7.23 *)
+Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C Fobj}(I:C) :=
+{ mon_f := F
+; mon_i := I
+; mon_c := C
+(*; mon_bin := BinoidalCat_from_Bifunctor mon_f*)
+; mon_first := fun a b c (f:a~>b) => F \ pair_mor (pair_obj a c) (pair_obj b c) f (id c)
+; mon_second := fun a b c (f:a~>b) => F \ pair_mor (pair_obj c a) (pair_obj c b) (id c) f
+; mon_cancelr : (func_rlecnac I >>>> F) <~~~> functor_id C
+; mon_cancell : (func_llecnac I >>>> F) <~~~> functor_id C
+; mon_assoc : ((F **** (functor_id C)) >>>> F) <~~~> func_cossa >>>> ((((functor_id C) **** F) >>>> F))
+; mon_pentagon : Pentagon mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
+; mon_triangle : Triangle mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
+ (fun a => #(mon_cancell a)) (fun a => #(mon_cancelr a))
+}.
+
+(* FIXME: show that the endofunctors on any given category form a monoidal category *)
+
+(* Coq manual on coercions: ... only the oldest one is valid and the
+ * others are ignored. So the order of declaration of coercions is
+ * important. *)
+Coercion mon_c : MonoidalCat >-> Category.
+(*Coercion mon_bin : MonoidalCat >-> BinoidalCat.*)
+Coercion mon_f : MonoidalCat >-> Functor.
+Implicit Arguments mon_f [Ob Hom C Fobj F I].
+Implicit Arguments mon_i [Ob Hom C Fobj F I].
+Implicit Arguments mon_c [Ob Hom C Fobj F I].
+(*Implicit Arguments mon_bin [Ob Hom C Fobj F I].*)
+Implicit Arguments MonoidalCat [Ob Hom ].
+
+Section MonoidalCat_is_PreMonoidal.
+ Context `(M:MonoidalCat).
+ Definition mon_bin_M := BinoidalCat_from_Bifunctor (mon_f M).
+ Existing Instance mon_bin_M.
+ Lemma mon_pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a).
+ intros.
+ set (fun c => mon_assoc (pair_obj (pair_obj a c) b)) as qq.
+ simpl in qq.
+ apply Build_NaturalIsomorphism with (ni_iso:=qq).
+ abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
+ (pair_mor (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
+ (pair_mor (pair_obj a A) (pair_obj a B) (id a) f) (id b))) as qr;
+ apply qr).
+ Defined.
+
+ Lemma mon_pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b).
+ intros.
+ set (fun c:C => mon_assoc (pair_obj (pair_obj c a) b)) as qq.
+ simpl in qq.
+ apply ni_inv.
+ apply Build_NaturalIsomorphism with (ni_iso:=qq).
+ abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
+ (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
+ (pair_mor (pair_obj _ _) (pair_obj _ _) f (id a)) (id b))) as qr;
+ etransitivity; [ idtac | apply qr ];
+ apply comp_respects; try reflexivity;
+ unfold mon_f;
+ simpl;
+ apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
+ split; try reflexivity;
+ symmetry;
+ simpl;
+ set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
+ simpl in qqqq;
+ apply qqqq).
+ Defined.
+
+ Lemma mon_pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a).
+ intros.
+ set (fun c:C => mon_assoc (pair_obj (pair_obj a b) c)) as qq.
+ simpl in qq.
+ set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (Fobj (pair_obj a b) ⋊-) (b ⋊- >>>> a ⋊-)) as qqq.
+ set (qqq qq) as q'.
+ apply q'.
+ clear q'.
+ clear qqq.
+ abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
+ (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
+ (pair_mor (pair_obj _ _) (pair_obj _ _) (id a) (id b)) f)) as qr;
+ etransitivity; [ apply qr | idtac ];
+ apply comp_respects; try reflexivity;
+ unfold mon_f;
+ simpl;
+ apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
+ split; try reflexivity;
+ simpl;
+ set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
+ simpl in qqqq;
+ apply qqqq).
+ Defined.
+
+ Lemma mon_pmon_cancelr : (bin_first I0) <~~~> functor_id C.
+ set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_first I0) (functor_id C)) as qq.
+ set (mon_cancelr) as z.
+ simpl in z.
+ simpl in qq.
+ set (qq z) as zz.
+ apply zz.
+ abstract (intros;
+ set (ni_commutes mon_cancelr) as q; simpl in *;
+ apply q).
+ Defined.
+
+ Lemma mon_pmon_cancell : (bin_second I0) <~~~> functor_id C.
+ set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_second I0) (functor_id C)) as qq.
+ set (mon_cancell) as z.
+ simpl in z.
+ simpl in qq.
+ set (qq z) as zz.
+ apply zz.
+ abstract (intros;
+ set (ni_commutes mon_cancell) as q; simpl in *;
+ apply q).
+ Defined.
+
+ Lemma mon_pmon_triangle : forall a b, #(mon_pmon_cancelr a) ⋉ b ~~ #(mon_pmon_assoc _ _ _) >>> a ⋊ #(mon_pmon_cancell b).
+ intros.
+ set mon_triangle as q.
+ simpl in q.
+ apply q.
+ Qed.
+
+ Lemma mon_pmon_pentagon a b c d : (#(mon_pmon_assoc a c b ) ⋉ d) >>>
+ #(mon_pmon_assoc a d _ ) >>>
+ (a ⋊ #(mon_pmon_assoc b d c))
+ ~~ #(mon_pmon_assoc _ d c ) >>>
+ #(mon_pmon_assoc a _ b ).
+ set (@pentagon _ _ _ _ _ _ _ mon_pentagon) as x.
+ simpl in x.
+ unfold bin_obj.
+ unfold mon_first in x.
+ simpl in *.
+ apply x.
+ Qed.
+
+ Definition MonoidalCat_is_PreMonoidal : PreMonoidalCat (BinoidalCat_from_Bifunctor (mon_f M)) (mon_i M).
+ refine {| pmon_assoc := mon_pmon_assoc
+ ; pmon_cancell := mon_pmon_cancell
+ ; pmon_cancelr := mon_pmon_cancelr
+ ; pmon_triangle := {| triangle := mon_pmon_triangle |}
+ ; pmon_pentagon := {| pentagon := mon_pmon_pentagon |}
+ ; pmon_assoc_ll := mon_pmon_assoc_ll
+ ; pmon_assoc_rr := mon_pmon_assoc_rr
+ |}.
+ abstract (set (coincide mon_triangle) as qq; simpl in *; apply qq).
+ abstract (intros; simpl; reflexivity).
+ abstract (intros; simpl; reflexivity).
+ Defined.
+
+ Lemma MonoidalCat_all_central : forall a b (f:a~~{M}~~>b), CentralMorphism f.
+ intros;
+ set (@fmor_preserves_comp _ _ _ _ _ _ _ M) as fc.
+ apply Build_CentralMorphism;
+ intros; simpl in *.
+ etransitivity.
+ apply fc.
+ symmetry.
+ etransitivity.
+ apply fc.
+ apply (fmor_respects M).
+ simpl.
+ setoid_rewrite left_identity;
+ setoid_rewrite right_identity;
+ split; reflexivity.
+ etransitivity.
+ apply fc.
+ symmetry.
+ etransitivity.
+ apply fc.
+ apply (fmor_respects M).
+ simpl.
+ setoid_rewrite left_identity;
+ setoid_rewrite right_identity;
+ split; reflexivity.
+ Qed.
+
+End MonoidalCat_is_PreMonoidal.
+
+Hint Extern 1 => apply MonoidalCat_all_central.
+Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
+(*Lemma CommutativePreMonoidalCategoriesAreMonoidal `(pm:PreMonoidalCat)(cc:CommutativeCat pm) : MonoidalCat pm.*)
+
+Section MonoidalFunctor.
+ Context `(m1:MonoidalCat(C:=C1)) `(m2:MonoidalCat(C:=C2)).
+ Class MonoidalFunctor {Mobj:C1->C2} (mf_F:Functor C1 C2 Mobj) :=
+ { mf_f := mf_F where "f ⊕⊕ g" := (@fmor _ _ _ _ _ _ _ m2 _ _ (pair_mor (pair_obj _ _) (pair_obj _ _) f g))
+ ; mf_coherence : (mf_F **** mf_F) >>>> (mon_f m2) <~~~> (mon_f m1) >>>> mf_F
+ ; mf_phi := fun a b => #(mf_coherence (pair_obj a b))
+ ; mf_id : (mon_i m2) ≅ (mf_F (mon_i m1))
+ ; mf_cancelr : forall a, #(mon_cancelr(MonoidalCat:=m2) (mf_F a)) ~~
+ (id (mf_F a)) ⊕⊕ #mf_id >>> mf_phi a (mon_i _) >>> mf_F \ #(mon_cancelr a)
+ ; mf_cancell : forall b, #(mon_cancell (mf_F b)) ~~
+ #mf_id ⊕⊕ (id (mf_F b)) >>> mf_phi (mon_i _) b >>> mf_F \ #(mon_cancell b)
+ ; mf_assoc : forall a b c, (mf_phi a b) ⊕⊕ (id (mf_F c)) >>> (mf_phi _ c) >>>
+ (mf_F \ #(mon_assoc (pair_obj (pair_obj a b) c) )) ~~
+ #(mon_assoc (pair_obj (pair_obj _ _) _) ) >>>
+ (id (mf_F a)) ⊕⊕ (mf_phi b c) >>> (mf_phi a _)
+ }.
+End MonoidalFunctor.
+Coercion mf_f : MonoidalFunctor >-> Functor.
+Implicit Arguments mf_coherence [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
+Implicit Arguments mf_id [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
+
+Section MonoidalFunctorsCompose.
+ Context `(m1:MonoidalCat).
+ Context `(m2:MonoidalCat).
+ Context `(m3:MonoidalCat).
+ Context {f1obj}(f1:@Functor _ _ m1 _ _ m2 f1obj).
+ Context {f2obj}(f2:@Functor _ _ m2 _ _ m3 f2obj).
+ Context (mf1:MonoidalFunctor m1 m2 f1).
+ Context (mf2:MonoidalFunctor m2 m3 f2).
+
+ Lemma mf_compose_coherence : (f1 >>>> f2) **** (f1 >>>> f2) >>>> m3 <~~~> m1 >>>> (f1 >>>> f2).
+ set (mf_coherence mf1) as mc1.
+ set (mf_coherence mf2) as mc2.
+ set (@ni_comp) as q.
+ set (q _ _ _ _ _ _ _ ((f1 >>>> f2) **** (f1 >>>> f2) >>>> m3) _ ((f1 **** f1 >>>> m2) >>>> f2) _ (m1 >>>> (f1 >>>> f2))) as qq.
+ apply qq; clear qq; clear q.
+ apply (@ni_comp _ _ _ _ _ _ _ _ _ (f1 **** f1 >>>> (f2 **** f2 >>>> m3)) _ _).
+ apply (@ni_comp _ _ _ _ _ _ _ _ _ ((f1 **** f1 >>>> f2 **** f2) >>>> m3) _ _).
+ eapply ni_respects.
+ apply ni_prod_comp.
+ apply ni_id.
+ apply ni_associativity.
+ apply ni_inv.
+ eapply ni_comp.
+ apply (ni_associativity (f1 **** f1) m2 f2).
+ apply (ni_respects (F0:=f1 **** f1)(F1:=f1 **** f1)(G0:=(m2 >>>> f2))(G1:=(f2 **** f2 >>>> m3))).
+ apply ni_id.
+ apply ni_inv.
+ apply mc2.
+ apply ni_inv.
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity m1 f1 f2).
+ apply ni_respects.
+ apply ni_inv.
+ apply mc1.
+ apply ni_id.
+ Qed.
+
+ Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
+ { mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
+ ; mf_coherence := mf_compose_coherence
+ }.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+End MonoidalFunctorsCompose.
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+
+(*******************************************************************************)
+(* Chapter 7.5: Natural Isomorphisms *)
+(*******************************************************************************)
+
+(* Definition 7.10 *)
+Class NaturalIsomorphism `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
+{ ni_iso : forall A, Fobj1 A ≅ Fobj2 A
+; ni_commutes : forall `(f:A~>B), #(ni_iso A) >>> F2 \ f ~~ F1 \ f >>> #(ni_iso B)
+}.
+Implicit Arguments ni_iso [Ob Hom Ob0 Hom0 C1 C2 Fobj1 Fobj2 F1 F2].
+Implicit Arguments ni_commutes [Ob Hom Ob0 Hom0 C1 C2 Fobj1 Fobj2 F1 F2 A B].
+(* FIXME: coerce to NaturalTransformation instead *)
+Coercion ni_iso : NaturalIsomorphism >-> Funclass.
+Notation "F <~~~> G" := (@NaturalIsomorphism _ _ _ _ _ _ _ _ F G) : category_scope.
+
+(* FIXME: Lemma 7.11: natural isos are natural transformations in which every morphism is an iso *)
+
+(* every natural iso is invertible, and that inverse is also a natural iso *)
+Definition ni_inv `(N:NaturalIsomorphism(F1:=F1)(F2:=F2)) : NaturalIsomorphism F2 F1.
+ intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F2 F1 (fun A => iso_inv _ _ (ni_iso N A))).
+ abstract (intros; simpl;
+ set (ni_commutes N f) as qqq;
+ symmetry in qqq;
+ apply iso_shift_left' in qqq;
+ setoid_rewrite qqq;
+ repeat setoid_rewrite <- associativity;
+ setoid_rewrite iso_comp2;
+ setoid_rewrite left_identity;
+ reflexivity).
+ Defined.
+
+Definition ni_id
+ `{C1:Category}`{C2:Category}
+ {Fobj}(F:Functor C1 C2 Fobj)
+ : NaturalIsomorphism F F.
+ intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F F (fun A => iso_id (F A))).
+ abstract (intros; simpl; setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+ Defined.
+
+(* two different choices of composition order are naturally isomorphic (strictly, in fact) *)
+Instance ni_associativity
+ `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}
+ {Fobj1}(F1:Functor C1 C2 Fobj1)
+ {Fobj2}(F2:Functor C2 C3 Fobj2)
+ {Fobj3}(F3:Functor C3 C4 Fobj3)
+ :
+ ((F1 >>>> F2) >>>> F3) <~~~> (F1 >>>> (F2 >>>> F3)) :=
+ { ni_iso := fun A => iso_id (F3 (F2 (F1 A))) }.
+ abstract (intros;
+ simpl;
+ setoid_rewrite left_identity;
+ setoid_rewrite right_identity;
+ reflexivity).
+ Defined.
+
+Definition ni_comp `{C:Category}`{D:Category}
+ {F1Obj}{F1:@Functor _ _ C _ _ D F1Obj}
+ {F2Obj}{F2:@Functor _ _ C _ _ D F2Obj}
+ {F3Obj}{F3:@Functor _ _ C _ _ D F3Obj}
+ (N1:NaturalIsomorphism F1 F2)
+ (N2:NaturalIsomorphism F2 F3)
+ : NaturalIsomorphism F1 F3.
+ 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)).
+ abstract (intros; simpl;
+ setoid_rewrite <- associativity;
+ setoid_rewrite <- ni_commutes1;
+ setoid_rewrite associativity;
+ setoid_rewrite <- ni_commutes2;
+ reflexivity).
+ 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}
+ : (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))) |}.
+ abstract (intros; simpl;
+ setoid_rewrite <- associativity;
+ setoid_rewrite fmor_preserves_comp;
+ setoid_rewrite <- phi_comm;
+ setoid_rewrite <- fmor_preserves_comp;
+ setoid_rewrite associativity;
+ apply comp_respects; try reflexivity;
+ apply psi_comm).
+ Defined.
+
+(*
+ * Some structures (like monoidal and premonoidal functors) use the isomorphism
+ * component of a natural isomorphism in an "informative" way; these structures
+ * should use NaturalIsomorphism.
+ *
+ * However, in other situations the actual iso used is irrelevant; all
+ * that matters is the fact that a natural family of them exists. In
+ * these cases we can speed up Coq (and the extracted program)
+ * considerably by making the family of isos belong to [Prop] rather
+ * than [Type]. IsomorphicFunctors does this -- it's essentially a
+ * copy of NaturalIsomorphism which lives in [Prop].
+ *)
+
+(* Definition 7.10 *)
+Definition IsomorphicFunctors `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
+ exists ni_iso : (forall A, Fobj1 A ≅ Fobj2 A),
+ forall `(f:A~>B), #(ni_iso A) >>> F2 \ f ~~ F1 \ f >>> #(ni_iso B).
+Notation "F ≃ G" := (@IsomorphicFunctors _ _ _ _ _ _ _ _ F G) : category_scope.
+
+Definition if_id `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj) : IsomorphicFunctors F F.
+ exists (fun A => iso_id (F A)).
+ abstract (intros;
+ simpl;
+ etransitivity;
+ [ apply left_identity |
+ symmetry;
+ apply right_identity]).
+ Qed.
+
+(* every natural iso is invertible, and that inverse is also a natural iso *)
+Definition if_inv
+ `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}{F1:Functor C1 C2 Fobj1}{F2:Functor C1 C2 Fobj2}
+ (N:IsomorphicFunctors F1 F2) : IsomorphicFunctors F2 F1.
+ intros.
+ destruct N as [ ni_iso ni_commutes ].
+ exists (fun A => iso_inv _ _ (ni_iso A)).
+ intros; simpl.
+ symmetry.
+ set (ni_commutes _ _ f) as qq.
+ symmetry in qq.
+ apply iso_shift_left' in qq.
+ setoid_rewrite qq.
+ repeat setoid_rewrite <- associativity.
+ setoid_rewrite iso_comp2.
+ setoid_rewrite left_identity.
+ reflexivity.
+ Qed.
+
+Definition if_comp `{C:Category}`{D:Category}
+ {F1Obj}{F1:@Functor _ _ C _ _ D F1Obj}
+ {F2Obj}{F2:@Functor _ _ C _ _ D F2Obj}
+ {F3Obj}{F3:@Functor _ _ C _ _ D F3Obj}
+ (N1:IsomorphicFunctors F1 F2)
+ (N2:IsomorphicFunctors F2 F3)
+ : IsomorphicFunctors F1 F3.
+ 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)).
+ abstract (intros; simpl;
+ setoid_rewrite <- associativity;
+ setoid_rewrite <- ni_commutes1;
+ setoid_rewrite associativity;
+ setoid_rewrite <- ni_commutes2;
+ reflexivity).
+ Qed.
+
+(* two different choices of composition order are naturally isomorphic (strictly, in fact) *)
+Definition if_associativity
+ `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}
+ {Fobj1}(F1:Functor C1 C2 Fobj1)
+ {Fobj2}(F2:Functor C2 C3 Fobj2)
+ {Fobj3}(F3:Functor C3 C4 Fobj3)
+ :
+ ((F1 >>>> F2) >>>> F3) ≃ (F1 >>>> (F2 >>>> F3)).
+ exists (fun A => iso_id (F3 (F2 (F1 A)))).
+ abstract (intros;
+ simpl;
+ setoid_rewrite left_identity;
+ setoid_rewrite right_identity;
+ reflexivity).
+ Defined.
+
+Definition if_left_identity `{C1:Category}`{C2:Category} {Fobj1}(F1:Functor C1 C2 Fobj1) : (functor_id _ >>>> F1) ≃ F1.
+ exists (fun a => iso_id (F1 a)).
+ abstract (intros; unfold functor_comp; simpl;
+ setoid_rewrite left_identity;
+ setoid_rewrite right_identity;
+ reflexivity).
+ Defined.
+
+Definition if_right_identity `{C1:Category}`{C2:Category} {Fobj1}(F1:Functor C1 C2 Fobj1) : (F1 >>>> functor_id _) ≃ F1.
+ exists (fun a => iso_id (F1 a)).
+ abstract (intros; unfold functor_comp; simpl;
+ setoid_rewrite left_identity;
+ setoid_rewrite right_identity;
+ reflexivity).
+ 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}
+ : (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))).
+ abstract (intros; simpl;
+ setoid_rewrite <- associativity;
+ setoid_rewrite fmor_preserves_comp;
+ setoid_rewrite <- phi_comm;
+ setoid_rewrite <- fmor_preserves_comp;
+ setoid_rewrite associativity;
+ apply comp_respects; try reflexivity;
+ apply psi_comm).
+ Defined.
+
+Section ni_prod_comp.
+ Context
+ `{C1:Category}`{C2:Category}
+ `{D1:Category}`{D2:Category}
+ {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}.
+
+ Definition ni_prod_comp_iso A : (((F1 >>>> G1) **** (F2 >>>> G2)) A) ≅ (((F1 **** F2) >>>> (G1 **** G2)) A).
+ unfold functor_fobj.
+ unfold functor_product_fobj.
+ simpl.
+ apply iso_id.
+ Defined.
+
+ Lemma ni_prod_comp : (F1 >>>> G1) **** (F2 >>>> G2) <~~~> (F1 **** F2) >>>> (G1 **** G2).
+ refine {| ni_iso := ni_prod_comp_iso |}.
+ intros.
+ destruct A.
+ destruct B.
+ simpl.
+ setoid_rewrite left_identity.
+ setoid_rewrite right_identity.
+ split; reflexivity.
+ Defined.
+End ni_prod_comp.
--- /dev/null
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 9.8: Natural Numbers Object *)
+(*******************************************************************************)
+
+
+
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+
+(*******************************************************************************)
+(* Chapter 7.4: Natural Transformations *)
+(*******************************************************************************)
+
+(* Definition 7.6 *)
+Structure NaturalTransformation `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
+{ nt_component : forall c:C1, (Fobj1 c) ~~{C2}~~> (Fobj2 c)
+; nt_commutes : forall `(f:A~>B), (nt_component A) >>> F2 \ f ~~ F1 \ f >>> (nt_component B)
+}.
+Notation "F ~~~> G" := (@NaturalTransformation _ _ _ _ _ _ _ _ F G) : category_scope.
+Coercion nt_component : NaturalTransformation >-> Funclass.
+
+(* the identity natural transformation *)
+Definition nt_id `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj) : NaturalTransformation F F.
+ apply (@Build_NaturalTransformation _ _ _ _ _ _ _ _ F F (fun c => id (F c))).
+ abstract (intros;
+ setoid_rewrite left_identity;
+ setoid_rewrite right_identity;
+ reflexivity).
+ Defined.
+Definition nt_comp `{C:Category}`{D:Category}
+ {Fobj}{F:Functor C D Fobj}
+ {Gobj}{G:Functor C D Gobj}
+ {Hobj}{H:Functor C D Hobj}
+ (nt_f_g:F ~~~> G) (nt_g_h:G ~~~> H) : F ~~~> H.
+ apply (@Build_NaturalTransformation _ _ _ _ _ _ _ _ F H (fun c => nt_f_g c >>> nt_g_h c)).
+ abstract (intros;
+ set (@nt_commutes _ _ C _ _ D _ _ F G nt_f_g) as comm1;
+ set (@nt_commutes _ _ C _ _ D _ _ G H nt_g_h) as comm2;
+ setoid_rewrite associativity;
+ setoid_rewrite comm2;
+ setoid_rewrite <- associativity;
+ setoid_rewrite <- comm1;
+ reflexivity).
+ Defined.
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+
+(******************************************************************************)
+(* Chapter 1.6.2: Opposite Categories *)
+(******************************************************************************)
+
+(* we don't want to register this as an instance, because it will confuse Coq *)
+Definition Opposite `(C:@Category Ob Hom) : Category Ob (fun x y => Hom y x).
+ intros.
+ apply (Build_Category Ob (fun x y => Hom y x)) with
+ (id := fun a => @id _ _ C a)
+ (comp := fun a b c f g => @comp _ _ C c b a g f)
+ (eqv := fun a b f g => @eqv _ _ C b a f g).
+
+ intros; apply Build_Equivalence;
+ [ unfold Reflexive; intros; reflexivity
+ | unfold Symmetric; intros; symmetry; auto
+ | unfold Transitive; intros; transitivity y; auto
+ ].
+ unfold Proper. intros. unfold respectful. intros. setoid_rewrite H. setoid_rewrite H0. reflexivity.
+ intros; apply (@right_identity _ _ C).
+ intros; apply (@left_identity _ _ C).
+ intros. symmetry; apply associativity.
+ Defined.
+Notation "C ⁽ºᑭ⁾" := (Opposite C) : category_scope.
+
+(* every functor between two categories determines a functor between their opposites *)
+Definition func_op `(F:Functor(c1:=c1)(c2:=c2)(fobj:=fobj)) : Functor c1⁽ºᑭ⁾ c2⁽ºᑭ⁾ fobj.
+ apply (@Build_Functor _ _ c1⁽ºᑭ⁾ _ _ c2⁽ºᑭ⁾ fobj (fun a b f => fmor F f)).
+ abstract (intros; apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H)).
+ abstract (intros; apply (@fmor_preserves_id _ _ _ _ _ _ _ F a)).
+ abstract (intros; apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f)).
+ Defined.
+
+(* we could do this by simply showing that (Opposite (Opposite C)) is isomorphic to C, but Coq distinguishes between
+ * two categories being *equal* versus merely isomorphic, so it's handy to be able to do this *)
+Definition func_opop `{c1:Category}`{c2:Category}{fobj}(F:Functor c1⁽ºᑭ⁾ c2⁽ºᑭ⁾ fobj) : Functor c1 c2 fobj.
+ apply (@Build_Functor _ _ c1 _ _ c2 fobj (fun a b f => fmor F f)).
+ abstract (intros; apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H)).
+ abstract (intros; apply (@fmor_preserves_id _ _ _ _ _ _ _ F a)).
+ abstract (intros; apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f)).
+ Defined.
+
+Definition func_op1 `{c1:Category}`{c2:Category}{fobj}(F:Functor c1⁽ºᑭ⁾ c2 fobj) : Functor c1 c2⁽ºᑭ⁾ fobj.
+ apply (@Build_Functor _ _ c1 _ _ c2⁽ºᑭ⁾ fobj (fun a b f => fmor F f)).
+ abstract (intros; apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H)).
+ abstract (intros; apply (@fmor_preserves_id _ _ _ _ _ _ _ F a)).
+ abstract (intros; apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f)).
+ Defined.
+
+Definition func_op2 `{c1:Category}`{c2:Category}{fobj}(F:Functor c1 c2⁽ºᑭ⁾ fobj) : Functor c1⁽ºᑭ⁾ c2 fobj.
+ apply (@Build_Functor _ _ c1⁽ºᑭ⁾ _ _ c2 fobj (fun a b f => fmor F f)).
+ abstract (intros; apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H)).
+ abstract (intros; apply (@fmor_preserves_id _ _ _ _ _ _ _ F a)).
+ abstract (intros; apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f)).
+ Defined.
+
--- /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.
--- /dev/null
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 9.7: Presheaves *)
+(*******************************************************************************)
+
+
+
+
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+
+(******************************************************************************)
+(* Chapter 1.6.1: Product Categories *)
+(******************************************************************************)
+
+Section ProductCategories.
+
+ Context `(C1:Category Ob1 Hom1).
+ Context `(C2:Category Ob2 Hom2).
+
+ (* trying to use the standard "prod" here causes a universe inconsistency once we get to coqBinoidal;
+ * moreover, using a general fully-polymorphic pair type seems to trigger some serious memory leaks
+ * in Coq *)
+ Inductive prod_obj : Type := pair_obj : C1 -> C2 -> prod_obj.
+ Definition fst_obj x := match x with pair_obj a _ => a end.
+ Definition snd_obj x := match x with pair_obj _ b => b end.
+
+ Inductive prod_mor (a b:prod_obj) : Type :=
+ pair_mor :
+ ((fst_obj a)~~{C1}~~>(fst_obj b)) ->
+ ((snd_obj a)~~{C2}~~>(snd_obj b)) ->
+ prod_mor a b.
+ Definition fst_mor {a b:prod_obj}(x:prod_mor a b) := match x with pair_mor a _ => a end.
+ Definition snd_mor {a b:prod_obj}(x:prod_mor a b) := match x with pair_mor _ b => b end.
+
+ Definition ProductCategory : Category prod_obj prod_mor.
+ refine
+ {| id := fun (a:prod_obj) => pair_mor a a (id (fst_obj a)) (id (snd_obj a))
+ ; comp := fun a b c (f:prod_mor a b) (g:prod_mor b c) =>
+ match f with pair_mor f1 f2 => match g with pair_mor g1 g2 => pair_mor _ _ (f1>>>g1) (f2>>>g2) end end
+ ; eqv := fun a b (f:prod_mor a b) (g:prod_mor a b) =>
+ match f with pair_mor f1 f2 => match g with pair_mor g1 g2 => (f1~~g1)/\(f2~~g2) end end
+ |}.
+ intros.
+ abstract (apply Build_Equivalence; intros; simpl; intros;
+ [ unfold Reflexive; intros; case x; intros; split; reflexivity
+ | unfold Symmetric; intros; destruct y; destruct x; split; case H; intros; symmetry; auto
+ | unfold Transitive; intros; destruct x; destruct z; destruct y; split; case H; case H0; intros; auto ]).
+ abstract (intros; unfold Proper; simpl; unfold respectful; intros;
+ destruct x0; destruct y0; destruct x; destruct y;
+ case H; intros; case H0; intros; split; auto).
+ abstract (intros; destruct a; destruct b; case f; intros; simpl; setoid_rewrite left_identity; split; reflexivity).
+ abstract (intros; destruct a; destruct b; case f; intros; simpl; setoid_rewrite right_identity; split; symmetry; reflexivity).
+ abstract (intros; destruct a; destruct b; destruct c; case f; intros; destruct d; simpl; case g; intros;
+ destruct h; setoid_rewrite associativity; split; reflexivity).
+ Defined.
+End ProductCategories.
+
+Implicit Arguments pair_obj [ Ob1 Hom1 Ob2 Hom2 C1 C2 ].
+Implicit Arguments pair_mor [ Ob1 Hom1 Ob2 Hom2 C1 C2 ].
+Notation "C ×× D" := (ProductCategory C D).
+
+Section ProductCategoryFunctors.
+
+ Context `{C:Category}.
+ Context `{D:Category}.
+
+ Definition func_pi1 : Functor (C ×× D) C (fun c => fst_obj _ _ c).
+ refine {| fmor := fun a b (f:prod_mor _ _ a b) => fst_mor _ _ f |}; intros; simpl in *.
+ destruct f; destruct f'; simpl in *; destruct H; auto.
+ reflexivity.
+ destruct f; destruct g; simpl in *; auto.
+ Defined.
+
+ Definition func_pi2 : Functor (C ×× D) D (fun c => snd_obj _ _ c).
+ refine {| fmor := fun a b (f:prod_mor _ _ a b) => snd_mor _ _ f |}; intros; simpl in *.
+ destruct f; destruct f'; simpl in *; destruct H; auto.
+ reflexivity.
+ destruct f; destruct g; simpl in *; auto.
+ Defined.
+
+ Definition llecnac_fmor (I:C) : forall (a b:D)(f:a~~{D}~~>b), (pair_obj I a)~~{C××D}~~>(pair_obj I b).
+ intros; apply pair_mor; [ exact (id I) | auto ].
+ Defined.
+ Definition func_llecnac (I:C) : Functor D (C ×× D) (pair_obj I).
+ refine {| fmor := fun a b f => llecnac_fmor I a b f |}.
+ abstract (intros; simpl; repeat split; simpl; auto).
+ abstract (intros; simpl; repeat split; simpl; auto).
+ abstract (intros; simpl; repeat split; simpl; auto).
+ Defined.
+
+ Definition rlecnac_fmor (I:D) : forall (a b:C)(f:a~~{C}~~>b), (pair_obj a I)~~{C××D}~~>(pair_obj b I).
+ intros; apply pair_mor; [ auto | exact (id I) ].
+ Defined.
+ Definition func_rlecnac (I:D) : Functor C (C ×× D) (fun c => (pair_obj c I)).
+ refine {| fmor := fun a b f => rlecnac_fmor I a b f |}.
+ abstract (intros; simpl; repeat split; simpl; auto).
+ abstract (intros; simpl; repeat split; simpl; auto).
+ abstract (intros; simpl; repeat split; simpl; auto).
+ Defined.
+
+ Context `{E:Category}.
+ Definition cossa : ((C ×× D) ×× E) -> (C ×× (D ×× E)).
+ intros.
+ case X as [a1 a2]; intros.
+ case a1 as [a11 a12]; intros.
+ exact (pair_obj a11 (pair_obj a12 a2)).
+ Defined.
+ Definition cossa_fmor (a:((C ×× D) ×× E)) (b:((C ×× D) ×× E)) (f:a~~{(C ×× D) ×× E}~~>b) : (cossa a)~~{C ×× (D ×× E)}~~>(cossa b).
+ case a as [ [a11 a12] a2];
+ case b as [ [b11 b12] b2];
+ case f as [ [f11 f12] f2];
+ apply pair_mor; auto;
+ apply pair_mor; auto.
+ Defined.
+ Definition func_cossa : Functor ((C ×× D) ×× E) (C ×× (D ×× E)) cossa.
+ refine {| fmor := fun a b f => cossa_fmor a b f |}.
+ abstract (intros;
+ case a as [ [a11 a12] a2];
+ case b as [ [b11 b12] b2];
+ case f as [ [f11 f12] f2];
+ case f' as [ [g11 g12] g2];
+ case H; intro H'; case H';
+ split; [ idtac | split ]; auto).
+ abstract (intros; case a as [ [a11 a12] a2]; split; [ idtac | split ]; reflexivity).
+ abstract (intros;
+ case a as [ [a11 a12] a2];
+ case b as [ [b11 b12] b2];
+ case c as [ [c11 c12] c2];
+ case f as [ [f11 f12] f2];
+ case g as [ [g11 g12] g2];
+ intros; reflexivity).
+ Defined.
+End ProductCategoryFunctors.
+
+Section func_prod.
+ Context `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}{Fobj1}{Fobj2}(F1:Functor C1 C2 Fobj1)(F2:Functor C3 C4 Fobj2).
+
+ Definition functor_product_fobj a := pair_obj (Fobj1 (fst_obj _ _ a)) (Fobj2 (snd_obj _ _ a)).
+
+ Definition functor_product_fmor (a b:(C1 ×× C3))(f:a~~{C1 ×× C3}~~>b)
+ : (functor_product_fobj a)~~{C2 ×× C4}~~>(functor_product_fobj b).
+ destruct a; intros.
+ destruct b; intros.
+ apply pair_mor; simpl;
+ [ apply (fmor F1) | apply (fmor F2) ];
+ case f; intros;
+ auto.
+ Defined.
+
+ Hint Unfold fst_obj.
+ Definition func_prod : Functor (C1 ×× C3) (C2 ×× C4) functor_product_fobj.
+ refine {| fmor := fun a b (f:a~~{C1 ×× C3}~~>b) => functor_product_fmor a b f |}.
+ abstract (intros; destruct a; try destruct b; destruct f; destruct f'; split; destruct H;
+ [ apply (@fmor_respects _ _ _ _ _ _ _ F1 _ _ h h1)
+ | apply (@fmor_respects _ _ _ _ _ _ _ F2 _ _ h0 h2)
+ ]; auto).
+ abstract (intros; case a; intros; simpl; split; apply fmor_preserves_id).
+ abstract (intros; destruct a; destruct b; destruct c; case f; intros; case g; intros; split; simpl; apply fmor_preserves_comp).
+ Defined.
+
+End func_prod.
+Notation "f **** g" := (func_prod f g).
+
+Instance iso_prod `{C:Category}`{D:Category}{a b:C}{c d:D}(ic:a≅b)(id:@Isomorphic _ _ D c d)
+ : @Isomorphic _ _ (C ×× D) (pair_obj a c) (pair_obj b d) :=
+ { iso_forward := pair_mor (pair_obj a c) (pair_obj b d) (iso_forward ic) (iso_forward id)
+ ; iso_backward := pair_mor (pair_obj b d) (pair_obj a c) (iso_backward ic) (iso_backward id)
+ }.
+ abstract (simpl; split; apply iso_comp1).
+ abstract (simpl; split; apply iso_comp2).
+ Defined.
+
+
+
--- /dev/null
+(*******************************************************************************)
+(* Chapter 7.2: Representable Structure *)
+(*******************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+Require Import Enrichment_ch2_8.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import MonoidalCategories_ch7_8.
+Require Import Coherence_ch7_8.
+
+(* FIXME: an object is a Generator if its covariant representable functor is faithful *)
+
+Section RepresentableStructure.
+ Context `(ec:ECategory(mn:=mn)(V:=V)).
+
+ Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell mn _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
+ Definition hom_covariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr mn _)⁻¹ >>> ((a ~~> d) ⋊ f) >>> ecomp.
+
+ Lemma hom_covariant_distributes {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
+ : hom_covariant (f >>> g) ~~ (hom_covariant (a:=x) f) >>> (hom_covariant g).
+ set (f >>> g) as fg; simpl in fg; unfold fg; clear fg.
+ unfold hom_covariant.
+ repeat setoid_rewrite associativity.
+ apply comp_respects; try reflexivity.
+ set (@ecomp_is_functorial) as qq.
+ repeat setoid_rewrite associativity in qq.
+ apply qq.
+ Qed.
+
+ Lemma hom_contravariant_distributes {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
+ : hom_contravariant (f >>> g) ~~ (hom_contravariant g) >>> (hom_contravariant (a:=x) f).
+ set (f >>> g) as fg; simpl in fg; unfold fg; clear fg.
+ unfold hom_contravariant.
+ repeat setoid_rewrite associativity.
+ etransitivity; [ idtac | symmetry; apply associativity ].
+ apply comp_respects; try reflexivity.
+ set (@ecomp_is_functorial _ _ _ _ _ _ _ _ _ _ _ _ _ x f g) as qq.
+ setoid_rewrite juggle2 in qq.
+ admit.
+ Qed.
+
+ Lemma hom_swap {a b c d:ec}(f:a~~{ec}~~>b)(g:c~~{ec}~~>d)
+ : hom_covariant f >>> hom_contravariant g ~~ hom_contravariant g >>> hom_covariant f.
+ etransitivity.
+ unfold hom_covariant.
+ unfold hom_contravariant.
+ Admitted.
+
+ Definition YonedaBiFunctor_fmor (a b:ec⁽ºᑭ⁾ ×× ec)(f:a~~{ec⁽ºᑭ⁾ ×× ec}~~>b)
+ : ((fst_obj _ _ a)~~>(snd_obj _ _ a))~~{V}~~>((fst_obj _ _ b)~~>(snd_obj _ _ b)).
+ destruct a as [a1 a2].
+ destruct b as [b1 b2].
+ case f as [f1 f2]; intros.
+ exact ( hom_contravariant (a:=a2) f1 >>> hom_covariant (a:=b1) f2 ).
+ Defined.
+
+ Definition YonedaBiFunctor : Functor (ec⁽ºᑭ⁾ ×× ec) V (fun a => (fst_obj _ _ a)~~>(snd_obj _ _ a)).
+ refine {| fmor := fun a b f => YonedaBiFunctor_fmor a b f |}.
+ abstract (intros; destruct a; destruct b; destruct f;
+ destruct f';
+ destruct H;
+ repeat (apply comp_respects; try reflexivity); simpl;
+ [ apply (@fmor_respects _ _ _ _ _ _ (fun x => (bin_obj x _))); auto
+ | apply (fmor_respects ((o1 ~~> o0) ⋊-)); auto ]).
+ abstract (
+ destruct a; unfold YonedaBiFunctor_fmor;
+ unfold hom_covariant;
+ unfold hom_contravariant;
+ etransitivity; simpl;
+ [ apply comp_respects; setoid_rewrite associativity; simpl;
+ [ etransitivity; [ apply comp_respects; [ reflexivity | apply eleft_identity ] | apply iso_comp2 ]
+ | etransitivity; [ apply comp_respects; [ reflexivity | apply eright_identity ] | apply iso_comp2 ]
+ ]
+ | apply left_identity ]
+ ).
+ abstract (destruct a; destruct b; destruct c;
+ destruct f;
+ destruct g; unfold YonedaBiFunctor_fmor;
+ setoid_rewrite juggle3;
+ setoid_rewrite hom_swap;
+ setoid_rewrite <- juggle3;
+ setoid_rewrite <- hom_contravariant_distributes;
+ setoid_rewrite <- hom_covariant_distributes;
+ simpl;
+ apply comp_respects;
+ reflexivity).
+ Defined.
+
+ Definition RepresentableFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
+ Definition RepresentableFunctor (X:ec) : Functor ec V (fun a => X~~>a) :=
+ func_llecnac(C:=ec⁽ºᑭ⁾)(D:=ec) X >>>> YonedaBiFunctor.
+
+ Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (RepresentableFunctor a \ f).
+ simpl.
+ setoid_rewrite <- associativity.
+ unfold hom_contravariant.
+ repeat setoid_rewrite <- associativity.
+ setoid_rewrite juggle1.
+ setoid_rewrite eleft_identity.
+ repeat setoid_rewrite <- associativity.
+ setoid_rewrite juggle1.
+ setoid_rewrite iso_comp1.
+ setoid_rewrite right_identity.
+ unfold hom_covariant.
+ repeat setoid_rewrite <- associativity.
+ set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (eid a)) as qq.
+ simpl in qq.
+ apply iso_shift_right' in qq.
+ apply symmetry in qq.
+ setoid_rewrite <- associativity in qq.
+ apply iso_shift_left' in qq.
+ apply symmetry in qq.
+ setoid_rewrite qq.
+ setoid_rewrite associativity.
+ setoid_rewrite juggle3.
+ setoid_rewrite (centralmor_first(CentralMorphism:=eid_central(ECategory:=ec) a)).
+ repeat setoid_rewrite associativity.
+ setoid_rewrite eleft_identity.
+ set (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn) f) as qqq.
+ simpl in qqq.
+ setoid_rewrite <- qqq.
+ setoid_rewrite <- associativity.
+ set (coincide pmon_triangle) as qqqq.
+ setoid_rewrite qqqq.
+ setoid_rewrite iso_comp1.
+ setoid_rewrite left_identity.
+ set (@eqv_equivalence) as qmt.
+ apply qmt.
+ Qed.
+
+
+End RepresentableStructure.
+Opaque RepresentableFunctor.
+
+Structure MonoidalEnrichment :=
+{ me_enr : Enrichment
+; me_fobj : prod_obj me_enr me_enr -> me_enr
+; me_f : Functor (me_enr ×× me_enr) me_enr me_fobj
+; me_i : me_enr
+; me_mon : MonoidalCat me_enr me_fobj me_f me_i
+; me_mf : MonoidalFunctor me_mon (enr_v_mon me_enr) (RepresentableFunctor me_enr me_i)
+}.
+Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
+Coercion me_enr : MonoidalEnrichment >-> Enrichment.
+
+(* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
+Structure MonicMonoidalEnrichment :=
+{ ffme_enr : MonoidalEnrichment
+; ffme_mf_full : FullFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr))
+; ffme_mf_faithful : FaithfulFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr))
+; ffme_mf_conservative : ConservativeFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr))
+}.
+Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
+Transparent RepresentableFunctor.
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+
+(******************************************************************************)
+(* Chapter 2.4: Sections and Retractions *)
+(******************************************************************************)
+
+(* FIXME: do sections as well *)
+
+Class RetractsInto `{C:Category} (A B:C) :=
+{ retract_embed : A~~{C}~~>B
+; retract_project : B~~{C}~~>A
+; retract_pf : retract_embed >>> retract_project ~~ id _
+}.
+Notation "A ⊆ B" := (@RetractsInto _ _ _ A B) (at level 100).
+Implicit Arguments retract_embed [ Ob Hom C A B ].
+Implicit Arguments retract_project [ Ob Hom C A B ].
+
+(* Remark 2.14 *)
+Instance FunctorsPreserveRetracts `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj){a b:C}(r:a ⊆ b) : ((Fobj a) ⊆ (Fobj b)) :=
+{ retract_embed := F \ (retract_embed r)
+; retract_project := F \ (retract_project r)
+}.
+ setoid_rewrite (fmor_preserves_comp F).
+ setoid_rewrite retract_pf.
+ apply fmor_preserves_id.
+ Defined.
+
+Instance iso_retract `{CX:Category}(a b:CX)(i:a ≅ b) : (a ⊆ b) :=
+{ retract_embed := iso_forward i
+; retract_project := iso_backward i
+}.
+ apply (iso_comp1 i).
+ Defined.
+
+Instance retract_comp `{CX:Category}(a b c:CX)(r1:a ⊆ b)(r2:b ⊆ c) : (a ⊆ c) :=
+{ retract_embed := (retract_embed r1) >>> (retract_embed r2)
+; retract_project := (retract_project r2) >>> (retract_project r1)
+}.
+ setoid_rewrite juggle3.
+ setoid_rewrite retract_pf.
+ setoid_rewrite right_identity.
+ apply retract_pf.
+ Defined.
+
+Instance retract_prod `{C:Category}`{D:Category}{a b:C}{d e:D}(r1:a ⊆ b)(r2:d ⊆ e)
+ : @RetractsInto _ _ (C ×× D) (pair_obj a d) (pair_obj b e) :=
+{ retract_embed := pair_mor (pair_obj a d) (pair_obj b e) (retract_embed r1) (retract_embed r2)
+; retract_project := pair_mor (pair_obj b e) (pair_obj a d) (retract_project r1) (retract_project r2)
+}.
+ simpl; split; apply retract_pf.
+ Defined.
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+
+(******************************************************************************)
+(* Chapter 1.6.4: Slice Categories *)
+(******************************************************************************)
+
+Definition MorphismInTo `{C:Category}(X:C) := { Y:C & Y~~{C}~~>X }.
+Definition MorphismOutOf `{C:Category}(X:C) := { Y:C & X~~{C}~~>Y }.
+
+Definition TriangleAbove `{C:Category}{X:C}(M1 M2:MorphismInTo X) :=
+ { f:(projT1 M1)~~{C}~~>(projT1 M2) & f >>> (projT2 M2) ~~ (projT2 M1) }.
+Definition TriangleBelow `{C:Category}{X:C}(M1 M2:MorphismOutOf X) :=
+ { f:(projT1 M1)~~{C}~~>(projT1 M2) & (projT2 M1) >>> f ~~ (projT2 M2) }.
+
+Program Instance SliceOver `(C:Category)(X:C) : Category (MorphismInTo X) TriangleAbove :=
+{ id := fun y1 => existT _ (id (projT1 y1)) _
+; eqv := fun a b f g => eqv _ _ (projT1 f) (projT1 g)
+; comp := fun _ _ _ f g => existT _ (projT1 f >>> projT1 g) _
+}.
+ Next Obligation.
+ destruct f. destruct g. destruct H0. destruct H1. simpl in *. setoid_rewrite <- e. setoid_rewrite <- e0. apply associativity.
+ Defined.
+ Next Obligation.
+ simpl; setoid_rewrite associativity. reflexivity.
+ Defined.
+
+Instance SliceOverInclusion `{C:Category}(X:C) : Functor (SliceOver C X) C (fun x => projT1 x) :=
+ { fmor := fun a b f => projT1 f }.
+ intros; simpl in H; auto.
+ intros. destruct a; simpl; auto.
+ intros. simpl. reflexivity.
+ Defined.
+
+Program Instance SliceUnder `(C:Category)(X:C) : Category (MorphismOutOf X) TriangleBelow :=
+{ id := fun y1 => existT _ (id (projT1 y1)) _
+; eqv := fun a b f g => eqv _ _ (projT1 f) (projT1 g)
+; comp := fun _ _ _ f g => existT _ (projT1 f >>> projT1 g) _
+}.
+ Next Obligation.
+ destruct f. destruct g. destruct H0. destruct H1. simpl in *. setoid_rewrite <- associativity.
+ setoid_rewrite e. auto.
+ Defined.
+ Next Obligation.
+ simpl; setoid_rewrite associativity. reflexivity.
+ Defined.
+
+Instance SliceUnderInclusion `{C:Category}(X:C) : Functor (SliceUnder C X) C (fun x => projT1 x) :=
+ { fmor := fun a b f => projT1 f }.
+ intros; simpl in H; auto.
+ intros. destruct a; simpl; auto.
+ intros. simpl. reflexivity.
+ Defined.
--- /dev/null
+(****************************************************************************)
+(* Chapter 7.1: Subcategories *)
+(****************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import OppositeCategories_ch1_6_2.
+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))
+}.
+
+(* 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.
+ Defined.
+
+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))
+ ; 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))
+ }.
+ intros; apply Build_Equivalence. unfold Reflexive.
+ intros; reflexivity.
+ unfold Symmetric; intros; simpl; symmetry; auto.
+ unfold Transitive; intros; simpl. transitivity (projT1 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.
+End SubCategoriesAreCategories.
+Coercion SubCategoriesAreCategories : SubCategory >-> 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.
+
+Definition FullImage `(F:Functor(c1:=C)(c2:=D)(fobj:=Fobj)) := FullSubcategory D (fun d => { c:C & (Fobj c)=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.
+ Defined.
+ Instance RestrictToImage : Functor C (FullImage F) RestrictToImage_fobj :=
+ { fmor := fun a b f => RestrictToImage_fmor a b 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.
+
+Instance func_opSubcat `(c1:Category Ob1 Hom1)`(c2:Category Ob Hom)`(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_respects _ _ _ _ _ _ _ F _ _ f f' H).
+ 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).
+ Context `(Cat2:Category O2 Hom2).
+ Context (Pobj:Cat2 -> Type).
+ Context (Pmor:forall a b:Cat2, (Pobj a) -> (Pobj b) -> (a~~{Cat2}~~>b) -> Type).
+ Context (SP:SubCategory Cat2 Pobj Pmor).
+ Context (Fobj:Cat1->Cat2).
+ Section Forward.
+ Context (F:Functor Cat1 Cat2 Fobj).
+ Context (pobj:forall a, Pobj (F a)).
+ Context (pmor:forall a b f, Pmor (F a) (F b) (pobj a) (pobj b) (F \ f)).
+ Definition FunctorWithRangeInSubCategory_fobj (X:Cat1) : SP :=
+ existT Pobj (Fobj X) (pobj X).
+ Definition FunctorWithRangeInSubCategory_fmor (dom ran:Cat1)(X:dom~>ran) : (@hom _ _ SP
+ (FunctorWithRangeInSubCategory_fobj dom) (FunctorWithRangeInSubCategory_fobj ran)).
+ intros.
+ exists (F \ X).
+ apply (pmor dom ran X).
+ Defined.
+ Definition FunctorWithRangeInSubCategory : Functor Cat1 SP FunctorWithRangeInSubCategory_fobj.
+ apply Build_Functor with (fmor:=FunctorWithRangeInSubCategory_fmor);
+ intros;
+ unfold FunctorWithRangeInSubCategory_fmor;
+ simpl.
+ setoid_rewrite H; auto.
+ apply (fmor_preserves_id F).
+ apply (fmor_preserves_comp F).
+ Defined.
+ End Forward.
+ Section Opposite.
+ Context (F:Functor Cat1 Cat2⁽ºᑭ⁾ Fobj).
+ Context (pobj:forall a, Pobj (F a)).
+ Context (pmor:forall a b f, Pmor (F b) (F a) (pobj b) (pobj a) (F \ f)).
+ Definition FunctorWithRangeInSubCategoryOp_fobj (X:Cat1) : SP :=
+ existT Pobj (Fobj X) (pobj X).
+ Definition FunctorWithRangeInSubCategoryOp_fmor (dom ran:Cat1)(X:dom~>ran) :
+ (FunctorWithRangeInSubCategoryOp_fobj dom)~~{SP⁽ºᑭ⁾}~~>(FunctorWithRangeInSubCategoryOp_fobj ran).
+ intros.
+ exists (F \ X).
+ apply (pmor dom ran X).
+ Defined.
+ (*
+ Definition FunctorWithRangeInSubCategoryOp : Functor Cat1 SP⁽ºᑭ⁾ FunctorWithRangeInSubCategoryOp_fobj.
+ apply Build_Functor with (fmor:=FunctorWithRangeInSubCategoryOp_fmor);
+ intros;
+ unfold FunctorWithRangeInSubCategoryOp_fmor;
+ simpl.
+ apply (fmor_respects(Functor:=F)); auto.
+ apply (fmor_preserves_id(Functor:=F)).
+ unfold eqv; simpl.
+ set (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ f _ g) as qq.
+ setoid_rewrite <- qq.
+ apply reflexivity.
+ Defined.
+ *)
+ End Opposite.
+End FunctorWithRangeInSubCategory.
+
+
+(* Definition 7.1: faithful functors *)
+Definition FaithfulFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
+ forall (a b:C1), forall (f f':a~>b), (fmor _ f)~~(fmor _ f') -> f~~f'.
+
+(* Definition 7.1: full functors *)
+Class FullFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
+ { ff_invert : forall {a b}(f:(Fobj a)~~{C2}~~>(Fobj b)) , { f' : a~~{C1}~~>b & (F \ f') ~~ f }
+ ; ff_respects : forall {a b}, Proper (eqv (Fobj a) (Fobj b) ==> eqv a b) (fun x => projT1 (@ff_invert a b x))
+ }.
+ Coercion ff_invert : FullFunctor >-> Funclass.
+
+(* Definition 7.1: (essentially) surjective on objects *)
+Definition EssentiallySurjectiveOnObjects `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
+ forall o2:C2, { o1:C1 & (F o1) ≅ o2 }.
+
+(* Definition 7.1: (essentially) injective on objects *)
+Class ConservativeFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
+ { cf_reflect_iso : forall (a b:C1), (F a) ≅ (F b) -> a ≅ b }.
+
+(* "monic up to natural iso" *)
+Definition WeaklyMonic
+ `{C:Category}
+ `{D:Category}
+ {Fobj}
+ (F:@Functor _ _ C _ _ D Fobj) := forall
+ `{E:Category}
+ `{G :@Functor _ _ E _ _ C Gobj'}
+ `{H :@Functor _ _ E _ _ C Hobj'},
+ G >>>> F ≃ H >>>> F
+ -> G ≃ H.
+
+Section FullFaithfulFunctor_section.
+ Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)).
+ Context (F_full:FullFunctor F).
+ Context (F_faithful:FaithfulFunctor F).
+
+ Lemma ff_functor_section_id_preserved : forall a:C1, projT1 (F_full _ _ (id (F a))) ~~ id a.
+ intros.
+ set (F_full a a (id (F a))) as qq.
+ destruct qq.
+ simpl.
+ apply F_faithful.
+ setoid_rewrite fmor_preserves_id.
+ auto.
+ Qed.
+
+ Definition ff_functor_section_fobj (a:FullImage F) : C1 := projT1 (projT2 a).
+
+ 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 ] ].
+ subst.
+ unfold ff_functor_section_fobj.
+ simpl.
+ destruct b as [ b1 [ b2 b3 ] ].
+ subst.
+ unfold ff_functor_section_fobj.
+ simpl.
+ apply (@ff_invert _ _ _ _ _ _ _ _ F_full).
+ apply f.
+ Defined.
+
+ Lemma ff_functor_section_respectful {a2 b2 c2 : C1}
+ (x0 : Fobj b2 ~~{ C2 }~~> Fobj c2)
+ (x : Fobj a2 ~~{ C2 }~~> Fobj b2) :
+ (let (x1, _) := F_full a2 b2 x in x1) >>>
+ (let (x1, _) := F_full b2 c2 x0 in x1) ~~
+ (let (x1, _) := F_full a2 c2 (x >>> x0) in x1).
+ set (F_full _ _ x) as x_full.
+ set (F_full _ _ x0) as x0_full.
+ set (F_full _ _ (x >>> x0)) as x_x0_full.
+ destruct x_full.
+ destruct x0_full.
+ destruct x_x0_full.
+ apply F_faithful.
+ setoid_rewrite e1.
+ setoid_rewrite <- (fmor_preserves_comp F).
+ setoid_rewrite e.
+ setoid_rewrite e0.
+ reflexivity.
+ Qed.
+
+ 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;
+ apply F_faithful;
+ etransitivity; [ apply e | idtac ];
+ symmetry;
+ etransitivity; [ apply e0 | idtac ];
+ symmetry; auto).
+ abstract (intros;
+ simpl;
+ destruct a as [ a1 [ a2 a3 ] ];
+ subst;
+ simpl;
+ apply ff_functor_section_id_preserved).
+ abstract (intros;
+ destruct a as [ a1 [ a2 a3 ] ];
+ destruct b as [ b1 [ b2 b3 ] ];
+ destruct c as [ c1 [ c2 c3 ] ];
+ subst;
+ simpl in *;
+ destruct f;
+ destruct g;
+ simpl in *;
+ apply ff_functor_section_respectful).
+ Defined.
+
+ Lemma ff_functor_section_splits_helper (a2 b2:C1)(f:existT (fun d : C2, {c : C1 & Fobj c = d}) (Fobj a2)
+ (existT (fun c : C1, Fobj c = Fobj a2) a2 (eq_refl _)) ~~{
+ 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.
+ simpl.
+ set (F_full a2 b2 x) as qq.
+ destruct qq.
+ apply e.
+ Qed.
+
+ Lemma ff_functor_section_splits : (ff_functor_section_functor >>>> RestrictToImage F) ~~~~ functor_id _.
+ unfold EqualFunctors.
+ intros.
+ simpl.
+ destruct a as [ a1 [ a2 a3 ] ].
+ destruct b as [ b1 [ b2 b3 ] ].
+ subst.
+ simpl in *.
+ inversion f; subst.
+ inversion f'; subst.
+ simpl in *.
+ apply heq_morphisms_intro.
+ simpl.
+ etransitivity; [ idtac | apply H ].
+ clear H.
+ clear f'.
+ apply ff_functor_section_splits_helper.
+ Qed.
+
+ Definition ff_functor_section_splits_niso_helper a : ((ff_functor_section_functor >>>> RestrictToImage F) a ≅ (functor_id (FullImage F)) a).
+ intros; simpl.
+ unfold functor_fobj.
+ unfold ff_functor_section_fobj.
+ unfold RestrictToImage_fobj.
+ destruct a as [ a1 [ a2 a3 ] ].
+ simpl.
+ subst.
+ unfold functor_fobj.
+ apply iso_id.
+ Defined.
+
+ Lemma ff_functor_section_splits_niso : (ff_functor_section_functor >>>> RestrictToImage F) ≃ functor_id _.
+ intros; simpl.
+ exists ff_functor_section_splits_niso_helper.
+ intros.
+ simpl in *.
+ destruct A as [ a1 [ a2 a3 ] ].
+ destruct B as [ b1 [ b2 b3 ] ].
+ simpl.
+ destruct f; subst.
+ simpl.
+ setoid_rewrite left_identity.
+ setoid_rewrite right_identity.
+ set (F_full a2 b2 x) as qr.
+ destruct qr.
+ symmetry; auto.
+ Qed.
+
+ Lemma ffc_functor_weakly_monic : ConservativeFunctor F -> WeaklyMonic F.
+ admit.
+ Qed.
+
+ Opaque ff_functor_section_splits_niso_helper.
+
+End FullFaithfulFunctor_section.
--- /dev/null
+(*******************************************************************************)
+(* Chapter 8: Yoneda *)
+(*******************************************************************************)
+
+ (*
+ Lemma YonedaLemma : forall (A B:ec), (CategoryOfNaturalTransformations (RepresentableFunctor A) (RepresentableFunctor B)) ≅ (B~~>A)
+ *)