From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Fri, 11 Mar 2011 07:59:30 +0000 (-0800)
Subject: initial checkin of coq-categories library
X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=ff3003c261295c60d367580b6700396102eb5a9c

initial checkin of coq-categories library
---

ff3003c261295c60d367580b6700396102eb5a9c
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..50dd02a
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+build/
+build/**
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..cb64606
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,17 @@
+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
diff --git a/src/Adjoints_ch9.v b/src/Adjoints_ch9.v
new file mode 100644
index 0000000..df870eb
--- /dev/null
+++ b/src/Adjoints_ch9.v
@@ -0,0 +1,55 @@
+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 *)
+
+
+
diff --git a/src/Algebras_ch4.v b/src/Algebras_ch4.v
new file mode 100644
index 0000000..b7f58d9
--- /dev/null
+++ b/src/Algebras_ch4.v
@@ -0,0 +1,246 @@
+(******************************************************************************)
+(* 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.
+
+
diff --git a/src/Categories_ch1_3.v b/src/Categories_ch1_3.v
new file mode 100644
index 0000000..e0a5838
--- /dev/null
+++ b/src/Categories_ch1_3.v
@@ -0,0 +1,81 @@
+(******************************************************************************)
+(* 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.
+
+
+
+
+
diff --git a/src/CategoryOfCategories_ch7_1.v b/src/CategoryOfCategories_ch7_1.v
new file mode 100644
index 0000000..77ed028
--- /dev/null
+++ b/src/CategoryOfCategories_ch7_1.v
@@ -0,0 +1,55 @@
+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.
diff --git a/src/CoEqualizers_ch3_4.v b/src/CoEqualizers_ch3_4.v
new file mode 100644
index 0000000..a56bb4d
--- /dev/null
+++ b/src/CoEqualizers_ch3_4.v
@@ -0,0 +1,9 @@
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+(******************************************************************************)
+(* Chapter 3.4: CoEqualizers                                                  *)
+(******************************************************************************)
+
+(* FIXME *)
diff --git a/src/Coherence_ch7_8.v b/src/Coherence_ch7_8.v
new file mode 100644
index 0000000..d683b90
--- /dev/null
+++ b/src/Coherence_ch7_8.v
@@ -0,0 +1,55 @@
+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 ].
diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v
new file mode 100644
index 0000000..32a7701
--- /dev/null
+++ b/src/Enrichment_ch2_8.v
@@ -0,0 +1,441 @@
+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.
+
diff --git a/src/EpicMonic_ch2_1.v b/src/EpicMonic_ch2_1.v
new file mode 100644
index 0000000..bc39509
--- /dev/null
+++ b/src/EpicMonic_ch2_1.v
@@ -0,0 +1,59 @@
+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.*)
+
diff --git a/src/Equalizers_ch3_3.v b/src/Equalizers_ch3_3.v
new file mode 100644
index 0000000..b4878d5
--- /dev/null
+++ b/src/Equalizers_ch3_3.v
@@ -0,0 +1,9 @@
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+(******************************************************************************)
+(* Chapter 3.3: Equalizers                                                    *)
+(******************************************************************************)
+
+(* FIXME *)
diff --git a/src/EquivalentCategories_ch7_8.v b/src/EquivalentCategories_ch7_8.v
new file mode 100644
index 0000000..7918cf3
--- /dev/null
+++ b/src/EquivalentCategories_ch7_8.v
@@ -0,0 +1,20 @@
+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 *)
diff --git a/src/Exponentials_ch6.v b/src/Exponentials_ch6.v
new file mode 100644
index 0000000..76f07bd
--- /dev/null
+++ b/src/Exponentials_ch6.v
@@ -0,0 +1,4 @@
+(*******************************************************************************)
+(* Closed Categories                                                           *)
+
+(*Definition ClosedCategory `(C:Category)(CI:C) :=*)
diff --git a/src/FreydAFT_ch9_8.v b/src/FreydAFT_ch9_8.v
new file mode 100644
index 0000000..a5cd59e
--- /dev/null
+++ b/src/FreydAFT_ch9_8.v
@@ -0,0 +1,9 @@
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 9.8: Freyd's Adjoint Functor Theorem                                *)
+(*******************************************************************************)
+
+
+
+
diff --git a/src/FunctorCategories_ch7_7.v b/src/FunctorCategories_ch7_7.v
new file mode 100644
index 0000000..1ed968c
--- /dev/null
+++ b/src/FunctorCategories_ch7_7.v
@@ -0,0 +1,90 @@
+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 *)
+
diff --git a/src/Functors_ch1_4.v b/src/Functors_ch1_4.v
new file mode 100644
index 0000000..78f4b59
--- /dev/null
+++ b/src/Functors_ch1_4.v
@@ -0,0 +1,114 @@
+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). *)
diff --git a/src/General.v b/src/General.v
new file mode 100644
index 0000000..ec5a797
--- /dev/null
+++ b/src/General.v
@@ -0,0 +1,602 @@
+(******************************************************************************)
+(* 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.
diff --git a/src/InitialTerminal_ch2_2.v b/src/InitialTerminal_ch2_2.v
new file mode 100644
index 0000000..af69c6a
--- /dev/null
+++ b/src/InitialTerminal_ch2_2.v
@@ -0,0 +1,34 @@
+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 *)
+
diff --git a/src/Isomorphisms_ch1_5.v b/src/Isomorphisms_ch1_5.v
new file mode 100644
index 0000000..fd9e19a
--- /dev/null
+++ b/src/Isomorphisms_ch1_5.v
@@ -0,0 +1,104 @@
+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.  
diff --git a/src/KanExtension_ch9_6.v b/src/KanExtension_ch9_6.v
new file mode 100644
index 0000000..7e059f8
--- /dev/null
+++ b/src/KanExtension_ch9_6.v
@@ -0,0 +1,5 @@
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 9.6: Kan Extensions                                                 *)
+(*******************************************************************************)
diff --git a/src/LCCCs_ch9_7.v b/src/LCCCs_ch9_7.v
new file mode 100644
index 0000000..1192aa9
--- /dev/null
+++ b/src/LCCCs_ch9_7.v
@@ -0,0 +1,9 @@
+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 *)
diff --git a/src/Main.v b/src/Main.v
new file mode 100644
index 0000000..2653fb8
--- /dev/null
+++ b/src/Main.v
@@ -0,0 +1,48 @@
+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.*)
diff --git a/src/Monads_ch10.v b/src/Monads_ch10.v
new file mode 100644
index 0000000..77405d3
--- /dev/null
+++ b/src/Monads_ch10.v
@@ -0,0 +1,9 @@
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 10: Monads                                                          *)
+(*******************************************************************************)
+
+
+
+
diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
new file mode 100644
index 0000000..920dc9d
--- /dev/null
+++ b/src/MonoidalCategories_ch7_8.v
@@ -0,0 +1,460 @@
+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.
diff --git a/src/NaturalIsomorphisms_ch7_5.v b/src/NaturalIsomorphisms_ch7_5.v
new file mode 100644
index 0000000..3371671
--- /dev/null
+++ b/src/NaturalIsomorphisms_ch7_5.v
@@ -0,0 +1,253 @@
+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.
diff --git a/src/NaturalNumbersObject_ch9_8.v b/src/NaturalNumbersObject_ch9_8.v
new file mode 100644
index 0000000..4ef1bd0
--- /dev/null
+++ b/src/NaturalNumbersObject_ch9_8.v
@@ -0,0 +1,9 @@
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 9.8: Natural Numbers Object                                         *)
+(*******************************************************************************)
+
+
+
+
diff --git a/src/NaturalTransformations_ch7_4.v b/src/NaturalTransformations_ch7_4.v
new file mode 100644
index 0000000..0fb6c41
--- /dev/null
+++ b/src/NaturalTransformations_ch7_4.v
@@ -0,0 +1,42 @@
+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.
+
diff --git a/src/OppositeCategories_ch1_6_2.v b/src/OppositeCategories_ch1_6_2.v
new file mode 100644
index 0000000..516334f
--- /dev/null
+++ b/src/OppositeCategories_ch1_6_2.v
@@ -0,0 +1,61 @@
+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.
+
diff --git a/src/Preamble.v b/src/Preamble.v
new file mode 100644
index 0000000..e360627
--- /dev/null
+++ b/src/Preamble.v
@@ -0,0 +1,142 @@
+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.
diff --git a/src/Presheaves_ch9_7.v b/src/Presheaves_ch9_7.v
new file mode 100644
index 0000000..2ada891
--- /dev/null
+++ b/src/Presheaves_ch9_7.v
@@ -0,0 +1,9 @@
+Generalizable All Variables.
+
+(*******************************************************************************)
+(* Chapter 9.7: Presheaves                                                     *)
+(*******************************************************************************)
+
+
+
+
diff --git a/src/ProductCategories_ch1_6_1.v b/src/ProductCategories_ch1_6_1.v
new file mode 100644
index 0000000..697641c
--- /dev/null
+++ b/src/ProductCategories_ch1_6_1.v
@@ -0,0 +1,170 @@
+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.
+
+
+
diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v
new file mode 100644
index 0000000..3dd7b78
--- /dev/null
+++ b/src/RepresentableStructure_ch7_2.v
@@ -0,0 +1,162 @@
+(*******************************************************************************)
+(* 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.
diff --git a/src/SectionRetract_ch2_4.v b/src/SectionRetract_ch2_4.v
new file mode 100644
index 0000000..3eda753
--- /dev/null
+++ b/src/SectionRetract_ch2_4.v
@@ -0,0 +1,56 @@
+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.
diff --git a/src/SliceCategories_ch1_6_4.v b/src/SliceCategories_ch1_6_4.v
new file mode 100644
index 0000000..a9d63df
--- /dev/null
+++ b/src/SliceCategories_ch1_6_4.v
@@ -0,0 +1,56 @@
+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.
diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v
new file mode 100644
index 0000000..ab876ca
--- /dev/null
+++ b/src/Subcategories_ch7_1.v
@@ -0,0 +1,342 @@
+(****************************************************************************)
+(* 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.
diff --git a/src/Yoneda_ch8.v b/src/Yoneda_ch8.v
new file mode 100644
index 0000000..045c427
--- /dev/null
+++ b/src/Yoneda_ch8.v
@@ -0,0 +1,7 @@
+(*******************************************************************************)
+(* Chapter 8: Yoneda                                                           *)
+(*******************************************************************************)
+
+  (*
+  Lemma YonedaLemma : forall (A B:ec), (CategoryOfNaturalTransformations (RepresentableFunctor A) (RepresentableFunctor B)) ≅ (B~~>A)
+  *)