From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sun, 3 Apr 2011 04:57:51 +0000 (+0000)
Subject: major revision: MonoidalCat is now a subclass of PreMonoidalCat
X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=27ffdd2265eb1c15acc62970f49d25a07bcadb05

major revision: MonoidalCat is now a subclass of PreMonoidalCat
---

diff --git a/src/BinoidalCategories.v b/src/BinoidalCategories.v
index ff08c3d..dddf786 100644
--- a/src/BinoidalCategories.v
+++ b/src/BinoidalCategories.v
@@ -3,7 +3,6 @@ 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 Subcategories_ch7_1.
 
 (******************************************************************************)
@@ -36,43 +35,3 @@ Class CommutativeCat `(BinoidalCat) :=
 }.
 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.
-  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.
diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v
index 84cc674..275de7b 100644
--- a/src/Enrichment_ch2_8.v
+++ b/src/Enrichment_ch2_8.v
@@ -26,16 +26,16 @@ Class ECategory `(mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI))(Eob:Type)(Ehom:Eob->Eo
 ; 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
+; 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))).
+   ((x ~~> a) ⋊-) \ (iso_backward (pmon_cancelr EI) >>> ((- ⋉EI) \ f >>> (((a ~~> b) ⋊-) \ g >>> ecomp))) >>> ecomp ~~
+   ((x ~~> a) ⋊-) \ f >>> (ecomp >>> (#(pmon_cancelr (x ~~> b)) ⁻¹ >>> (((x ~~> b) ⋊-) \ g >>> ecomp))).
 
    set (@fmor_preserves_comp) as fmor_preserves_comp'.
 
@@ -59,8 +59,8 @@ Lemma ecomp_is_functorial `{ec:ECategory}{a b c}{x}(f:EI~~{V}~~>(a~~>b))(g:EI~~{
    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) _ _))).
+    (#(pmon_assoc (x ~~> a) _ _)⁻¹ >>>
+     (bin_second(BinoidalCat:=bc) ((x ~~> a) ⊗ (a ~~> b))) \ g >>> #(pmon_assoc (x ~~> a) _ _))).
     symmetry.
 
     setoid_rewrite associativity.
@@ -119,8 +119,8 @@ Lemma ecomp_is_functorial `{ec:ECategory}{a b c}{x}(f:EI~~{V}~~>(a~~>b))(g:EI~~{
    (* 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 _).
+   setoid_replace (iso_backward ((pmon_cancelr) ((x ~~> a) ⊗ (a ~~> b)))) with
+     (iso_backward ((pmon_cancelr) ((x ~~> a) ⊗ (a ~~> b))) >>> id _).
    simpl.
    set (@iso_shift_right') as ibs.
    simpl in ibs.
@@ -147,8 +147,8 @@ Lemma ecomp_is_functorial `{ec:ECategory}{a b c}{x}(f:EI~~{V}~~>(a~~>b))(g:EI~~{
 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.
+   ((((#(pmon_cancelr EI) ⁻¹ >>> (f ⋉ EI >>> (a ~~> b) ⋊ g)) >>> ecomp) ⋉ EI >>> (a ~~> c) ⋊ h)) >>> ecomp ~~
+   ((f ⋉ EI >>> (a ~~> b) ⋊ ((#(pmon_cancelr EI) ⁻¹ >>> (g ⋉ EI >>> (b ~~> c) ⋊ h)) >>> ecomp))) >>> ecomp.
 
   intros; symmetry; etransitivity;
      [ setoid_rewrite associativity; apply comp_respects;
@@ -189,14 +189,14 @@ Lemma underlying_associativity `{ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Eh
 
   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.
+         (iso_backward (pmon_cancelr (a ~~> b)) ⋉ EI >>> ((a ~~> b) ⋊ g) ⋉ EI) ((a ~~> b) ⋊ g)
+         ((pmon_cancelr ((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.
+    set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) ((iso_backward (pmon_cancelr (a ~~> b)) >>> (a ~~> b) ⋊ g))) as qq.
     simpl in qq.
     setoid_rewrite <- qq.
     clear qq.
@@ -209,7 +209,7 @@ Lemma underlying_associativity `{ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Eh
 
 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
+; 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;
@@ -361,31 +361,19 @@ Instance UnderlyingFunctor `(EF:@EFunctor Ob Hom V bin_obj' bc EI mn Eob1 EHom1
   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
+Class EBinoidalCat `(ec:ECategory) :=
+{ ebc_bobj   : ec -> ec -> ec
+; ebc_first  : forall a:ec, EFunctor ec ec (fun x => ebc_bobj x a)
+; ebc_second : forall a:ec, EFunctor ec ec (fun x => ebc_bobj a x)
 }.
-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 (e:Enrichment) :=
-{ se_enr    := e
-; se_decomp :  @treeDecomposition (enr_v e) (option ((enr_c_obj e)*(enr_c_obj e)))
-                  (fun t => match t with
-                            | None   => enr_v_i e
-                            | Some x => match x with pair y z => enr_c_hom e y z end
-                            end)
-                  (fun d1 d2:enr_v e => enr_v_fobj e (pair_obj d1 d2))
-}.
-Coercion se_enr  : SurjectiveEnrichment >-> Enrichment.
+
+Instance EBinoidalCat_is_binoidal `(ebc:EBinoidalCat(ec:=ec)) : BinoidalCat (Underlying ec) ebc_bobj.
+  apply Build_BinoidalCat.
+  apply (fun a => UnderlyingFunctor (ebc_first a)).
+  apply (fun a => UnderlyingFunctor (ebc_second a)).
+  Defined.
+
+Coercion EBinoidalCat_is_binoidal : EBinoidalCat >-> BinoidalCat.
 
 (* Enriched Fibrations *)
 Section EFibration.
diff --git a/src/EquivalentCategories_ch7_8.v b/src/EquivalentCategories_ch7_8.v
index e5bcfb2..6ed769f 100644
--- a/src/EquivalentCategories_ch7_8.v
+++ b/src/EquivalentCategories_ch7_8.v
@@ -8,6 +8,7 @@ Require Import General.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
+Require Import NaturalIsomorphisms_ch7_5.
 
 (* Definition 7.24 *)
 Class EquivalentCategories `(C:Category)`(D:Category){Fobj}{Gobj}(F:Functor C D Fobj)(G:Functor D C Gobj) :=
diff --git a/src/FreydCategories.v b/src/FreydCategories.v
index c50e732..3e26e37 100644
--- a/src/FreydCategories.v
+++ b/src/FreydCategories.v
@@ -14,25 +14,29 @@ Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
+Require Import PreMonoidalCenter.
 Require Import MonoidalCategories_ch7_8.
 
 (* A Freyd Category is... *)
 Class FreydCategory
 
   (* a cartesian category C *)
-  `(C:CartesianCat(Ob:=Ob)(C:=C1)(Fobj:=fun x => bobj (fst_obj _ _ x) (snd_obj _ _ x)))
+  `(C:CartesianCat(Ob:=Ob)(C:=C1))
 
   (* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *)
   `(K:PreMonoidalCat(Ob:=Ob)(bin_obj':=bobj)(I:=@one _ _ _ C))
 
   (* an identity-on-objects functor J:C->Z(K) *)
-:= { fc_J       : Functor C (CenterMonoidal K) (fun x => exist _ x I)
+:= { fc_J       : Functor C (Center_is_Monoidal K) (fun x => exist (fun _ => True) x I)
 
   (* which is not only monoidal *)
-   ; fc_mf_J    : MonoidalFunctor C (CenterMonoidal K) fc_J
+   ; fc_mf_J    : MonoidalFunctor C (Center_is_Monoidal K) fc_J
 
-  (* but in fact strict (meaning the functor's coherence maps are identities) *)
-   ; fc_strict  : forall a, iso_forward (mf_coherence fc_mf_J a) ~~ id _
+   (* but in fact strict (meaning the functor's coherence maps are identities) *)
+   (*; fc_strict  : forall a b, #(mf_first a b) ~~ id _ 
+         FIXME - I will need to separate Subcategory from FullSubCategory in order to fix this *)
 
    ; fc_C       := C
    ; fc_K       := K
diff --git a/src/Main.v b/src/Main.v
index 962ed6d..de30773 100644
--- a/src/Main.v
+++ b/src/Main.v
@@ -24,25 +24,31 @@ Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 Require Import FunctorCategories_ch7_7.
 Require Import Coherence_ch7_8.
+
+Require Import PreMonoidalCategories.
+Require Import BinoidalCategories.
 Require Import MonoidalCategories_ch7_8.
+Require Import PreMonoidalCenter.
 
 Require Import Exponentials_ch6.
-(*Require Import CategoryOfCategories_ch7_1.*)
 Require Import Yoneda_ch8.
 Require Import Adjoints_ch9.
 
+(*Require Import CategoryOfCategories_ch7_1.*)
 (*Require Import PolynomialCategories.*)
 (*Require Import CoqCategory.*)
-(*Require Import NaturalDeduction.*)
-(*Require Import NaturalDeductionCategories.*)
 (*Require Import CartesianEnrichmentsHaveMonoidalHomFunctors.*)
-(*Require Import Reification.*)
-(*Require Import GeneralizedArrow.*)
-(*Require Import ReificationFromGArrow.*)
-(*Require Import GArrowFromReification.*)
-(*Require Import Roundtrip.*)
-(*Require Import RoundtripSlides.*)
+
+Require Import RepresentableStructure_ch7_2.
+
+Require Import EquivalentCategories_ch7_8.
+Require Import FreydAFT_ch9_8.
+Require Import KanExtension_ch9_6.
+Require Import LCCCs_ch9_7.
+Require Import Monads_ch10.
+Require Import NaturalNumbersObject_ch9_8.
+Require Import Presheaves_ch9_7.
 
 (* very slow! *)
-(*Require Import FreydCategories.*)
+Require Import FreydCategories.
 (*Require Import Arrows.*)
diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index d30346e..e9d3799 100644
--- a/src/MonoidalCategories_ch7_8.v
+++ b/src/MonoidalCategories_ch7_8.v
@@ -3,9 +3,9 @@ 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 ProductCategories_ch1_6_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 Require Import Coherence_ch7_8.
@@ -16,266 +16,143 @@ Require Import PreMonoidalCategories.
 (* Chapter 7.8: Monoidal Categories                                           *)
 (******************************************************************************)
 
-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_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))
-}.
-(* 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_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 MonoidalCat [Ob Hom ].
-
 (* TO DO: show that the endofunctors on any given category form a monoidal category *)
-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).
+(*
+ * Unlike Awodey, I define a monoidal category to be a premonoidal
+ * category in which all morphisms are central.  This is partly to
+ * have a clean inheritance hierarchy, but also because Coq bogs down
+ * on product categories for some inexplicable reason.
+ *)
+Class MonoidalCat `(pm:PreMonoidalCat) :=
+{ mon_pm          := pm
+; mon_commutative :> CommutativeCat pm
+}.
+Coercion mon_pm          : MonoidalCat >-> PreMonoidalCat.
+Coercion mon_commutative : MonoidalCat >-> CommutativeCat.
+
+(* a monoidal functor is just a premonoidal functor between premonoidal categories which happen to be monoidal *)
+Definition MonoidalFunctor `(m1:MonoidalCat) `(m2:MonoidalCat) := PreMonoidalFunctor m1 m2.
+
+Definition MonoidalFunctorsCompose
+  `{M1   :MonoidalCat(C:=C1)}
+  `{M2   :MonoidalCat(C:=C2)}
+   {fobj12:C1 -> C2                    }
+   (MF12 :MonoidalFunctor M1 M2 fobj12)
+  `{M3   :MonoidalCat(C:=C3)}
+   {fobj23:C2 -> C3                    }
+   (MF23 :MonoidalFunctor M2 M3 fobj23)
+   : MonoidalFunctor M1 M3 (fobj23 ○ fobj12).
+   apply PreMonoidalFunctorsCompose.
+   apply MF12.
+   apply MF23.
+   Defined.
 
-  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.
+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.
 
-  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.
+  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.
+  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 MonoidalFunctorsCompose.
+  (* if this binoidal structure has all of the natural isomorphisms of a premonoidal category, then it's monoidal *)
+  Context {pmI}(pm:PreMonoidalCat BinoidalCat_from_Bifunctor pmI).
 
-Section MonoidalCat_is_PreMonoidal.
-  Context `(M:MonoidalCat).
-  Definition mon_bin_M := BinoidalCat_from_Bifunctor (mon_f M).
-  Existing Instance mon_bin_M.
+  Instance PreMonoidalCat_from_bifunctor_is_Monoidal : MonoidalCat pm :=
+  { mon_commutative := Bifunctors_Create_Commutative_Binoidal_Categories
+  }.
 
-  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.
+End BinoidalCat_from_Bifunctor.
 
-  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.
+(* we can go the other way: given a monoidal category, its left/right functors can be combined into a bifunctor *)
+Section Bifunctor_from_MonoidalCat.
+  Context `(M:MonoidalCat).
 
-  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).
+  Definition Bifunctor_from_MonoidalCat_fobj : M ×× M -> M.
+    intro x.
+    destruct x.
+    exact (bin_obj' o o0).
     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.
+  Definition Bifunctor_from_MonoidalCat_fmor {a}{b}(f:a~~{M××M}~~>b)
+    : (Bifunctor_from_MonoidalCat_fobj a)~~{M}~~>(Bifunctor_from_MonoidalCat_fobj b).
+    destruct a; destruct b; destruct f.
     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).
+    apply (h ⋉ _ >>> _ ⋊ h0).
     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.
-
-(* Later: generalize to premonoidal categories *)
-Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
-{  copy_nt      :  forall a, functor_id _ ~~~> func_diagonal >>>> F
-;  copy         :  forall (a:mc),   a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
-                := fun a => nt_component _ _ (copy_nt a) a
+  Instance Bifunctor_from_MonoidalCat : Functor (M ×× M) M Bifunctor_from_MonoidalCat_fobj :=
+    { fmor := fun x y f => Bifunctor_from_MonoidalCat_fmor f }.
+    intros; simpl.
+    destruct a; destruct b; destruct f; destruct f'; simpl in *.
+    destruct H.
+    apply comp_respects.
+      apply (fmor_respects (-⋉o0)); auto.
+      apply (fmor_respects (o1⋊-)); auto.
+    intros; destruct a; simpl in *.
+      setoid_rewrite (fmor_preserves_id (-⋉o0)).
+      setoid_rewrite left_identity.
+      apply fmor_preserves_id.
+    intros; destruct a; destruct b; destruct c; destruct f; destruct g; simpl in *.
+      setoid_rewrite <- fmor_preserves_comp.
+      setoid_rewrite juggle3 at 1.
+      assert (CentralMorphism h1).
+        apply mon_commutative.
+      setoid_rewrite <- (centralmor_first(CentralMorphism:=H)).
+      setoid_rewrite <- juggle3.
+      reflexivity.
+      Defined.
+
+End Bifunctor_from_MonoidalCat.
+
+
+Class DiagonalCat `(mc:MonoidalCat) :=
+{ copy          :  forall (a:mc),   a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
+; copy_natural1 :  forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> f ⋉ a >>> b ⋊ f ~~ f >>> copy _
+; copy_natural2 :  forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> a ⋊ f >>> f ⋉ b ~~ f >>> copy _
 (* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
 }.
 
 Class CartesianCat `(mc:MonoidalCat) :=
-{ car_terminal  : Terminal mc
-; car_one       : (@one _ _ _ car_terminal) ≅ (mon_i mc)
-; car_diagonal  : DiagonalCat mc
-; car_law1      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
-; car_law2      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
+{ car_terminal  :> Terminal mc
+; car_one       :  one ≅ pmon_I
+; car_diagonal  :  DiagonalCat mc
+; car_law1      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell _))
+; car_law2      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr _))
 ; car_mn        := mc
 }.
 Coercion car_diagonal : CartesianCat >-> DiagonalCat.
diff --git a/src/NaturalIsomorphisms_ch7_5.v b/src/NaturalIsomorphisms_ch7_5.v
index 90ce326..415d13c 100644
--- a/src/NaturalIsomorphisms_ch7_5.v
+++ b/src/NaturalIsomorphisms_ch7_5.v
@@ -3,7 +3,6 @@ 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                                           *)
@@ -224,6 +223,7 @@ Definition if_respects
   Defined.
 
 Section ni_prod_comp.
+Require Import ProductCategories_ch1_6_1.
   Context
   `{C1:Category}`{C2:Category}
   `{D1:Category}`{D2:Category}
@@ -252,12 +252,3 @@ Section ni_prod_comp.
     Defined.
 End ni_prod_comp.
 
-Structure Retraction `{C:Category} `{D:Category} :=
-{ retraction_section_fobj       : C -> D
-; retraction_section            : Functor C D retraction_section_fobj
-; retraction_retraction_fobj    : D -> C
-; retraction_retraction         : Functor D C retraction_retraction_fobj
-; retraction_composes           : retraction_section >>>> retraction_retraction ≃ functor_id _
-}.
-Implicit Arguments Retraction [ [Ob] [Hom] [Ob0] [Hom0] ].
-Coercion retraction_section : Retraction >-> Functor.
diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v
index 7d9699b..e09f8ab 100644
--- a/src/PreMonoidalCategories.v
+++ b/src/PreMonoidalCategories.v
@@ -3,7 +3,6 @@ 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.
@@ -13,19 +12,22 @@ Require Import BinoidalCategories.
 
 (* 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)
+{ 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)
+; pmon_assoc_central   :  forall a b c, CentralMorphism #(pmon_assoc   a b c)
+; pmon_cancelr_central :  forall a    , CentralMorphism #(pmon_cancelr a)
+; pmon_cancell_central :  forall a    , CentralMorphism #(pmon_cancell a)
 }.
 (*
  * Premonoidal categories actually have three associators (the "f"
@@ -45,20 +47,20 @@ Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
  * 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 ].
+Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
+Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
+Implicit Arguments pmon_assoc   [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
 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).
+  : #(pmon_cancelr (a ⊗ b)) ~~ #((pmon_assoc a EI) b) >>> (a ⋊-) \ #(pmon_cancelr 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.
+  set (ni_commutes (pmon_assoc a b)) as xx.
   (* FIXME *)
   Admitted.
 
@@ -66,27 +68,187 @@ 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)
+{ mf_F          :> Functor C1 C2 fobj
+; mf_i          :  I2 ≅ mf_F I1
+; mf_first      :  ∀ a,              mf_F >>>> bin_first  (mf_F a)  <~~~>  bin_first  a >>>> mf_F
+; mf_second     :  ∀ a,              mf_F >>>> bin_second (mf_F a)  <~~~>  bin_second a >>>> mf_F
+; mf_consistent :  ∀ a b,            #(mf_first a b) ~~ #(mf_second b a)
+; mf_center     :  forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
+; mf_cancell    :  ∀ b,     #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first  b I1) >>> mf_F \ #(pmon_cancell b)
+; mf_cancelr    :  ∀ a,     #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a)
+; mf_assoc      :  ∀ a b c, #(pmon_assoc _ _ _)  >>> _ ⋊ #(mf_second _ _) >>>        #(mf_second _ _) ~~
+                            #(mf_second _ _) ⋉ _ >>>     #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b)
 }.
 Coercion mf_F : PreMonoidalFunctor >-> Functor.
 
+Definition PreMonoidalFunctorsCompose
+  `{PM1   :PreMonoidalCat(C:=C1)(I:=I1)}
+  `{PM2   :PreMonoidalCat(C:=C2)(I:=I2)}
+   {fobj12:C1 -> C2                    }
+   (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
+  `{PM3   :PreMonoidalCat(C:=C3)(I:=I3)}
+   {fobj23:C2 -> C3                    }
+   (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23)
+   : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12).
+   admit.
+   Defined.
+
 (*******************************************************************************)
 (* Braided and Symmetric Categories                                            *)
 
 Class BraidedCat `(mc:PreMonoidalCat) :=
 { br_niso        : forall a, bin_first a <~~~> bin_second a
 ; br_swap        := fun a b => ni_iso (br_niso 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
+; triangleb      : forall a:C,     #(pmon_cancelr a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell a)
+; hexagon1       : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _)
+                                   ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _)
+; hexagon2       : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹
+                                   ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
 }.
 
 Class SymmetricCat `(bc:BraidedCat) :=
 { symcat_swap  :  forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
 }.
+
+
+Section PreMonoidalSubCategory.
+
+  Context `(pm:PreMonoidalCat(I:=pmI)).
+  Context  {Pobj}{Pmor}(S:SubCategory pm Pobj Pmor).
+  Context  (Pobj_unit:Pobj pmI).
+  Context  (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
+  Implicit Arguments Pobj_closed [[a][b]].
+  Context  (Pmor_first: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
+                            Pmor _ _ (Pobj_closed pa pc) (Pobj_closed pb pc) (f ⋉ c)).
+  Context  (Pmor_second: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
+                            Pmor _ _ (Pobj_closed pc pa) (Pobj_closed pc pb) (c ⋊ f)).
+  Context  (Pmor_assoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
+                            Pmor _ _
+                            (Pobj_closed (Pobj_closed pa pb) pc)
+                            (Pobj_closed pa (Pobj_closed pb pc))
+                            #(pmon_assoc a c b)).
+  Context  (Pmor_unassoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
+                            Pmor _ _
+                            (Pobj_closed pa (Pobj_closed pb pc))
+                            (Pobj_closed (Pobj_closed pa pb) pc)
+                            #(pmon_assoc a c b)⁻¹).
+  Context  (Pmor_cancell: forall {a}(pa:Pobj a),
+                            Pmor _ _ (Pobj_closed Pobj_unit pa) pa 
+                            #(pmon_cancell a)).
+  Context  (Pmor_uncancell: forall {a}(pa:Pobj a),
+                            Pmor _ _ pa (Pobj_closed Pobj_unit pa)
+                            #(pmon_cancell a)⁻¹).
+  Context  (Pmor_cancelr: forall {a}(pa:Pobj a),
+                            Pmor _ _ (Pobj_closed pa Pobj_unit) pa 
+                            #(pmon_cancelr a)).
+  Context  (Pmor_uncancelr: forall {a}(pa:Pobj a),
+                            Pmor _ _ pa (Pobj_closed pa Pobj_unit)
+                            #(pmon_cancelr a)⁻¹).
+  Implicit Arguments Pmor_first [[a][b][c][f]].
+  Implicit Arguments Pmor_second [[a][b][c][f]].
+
+  Definition PreMonoidalSubCategory_bobj (x y:S) :=
+    existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
+
+  Definition PreMonoidalSubCategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+    (PreMonoidalSubCategory_bobj x a)~~{S}~~>(PreMonoidalSubCategory_bobj y a).
+    unfold hom; simpl; intros.
+    destruct f.
+    destruct a as [a apf].
+    destruct x as [x xpf].
+    destruct y as [y ypf].
+    simpl in *.
+    exists (x0 ⋉ a).
+    apply Pmor_first; auto.
+    Defined.
+
+  Definition PreMonoidalSubCategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+    (PreMonoidalSubCategory_bobj a x)~~{S}~~>(PreMonoidalSubCategory_bobj a y).
+    unfold hom; simpl; intros.
+    destruct f.
+    destruct a as [a apf].
+    destruct x as [x xpf].
+    destruct y as [y ypf].
+    simpl in *.
+    exists (a ⋊ x0).
+    apply Pmor_second; auto.
+    Defined.
+
+  Instance PreMonoidalSubCategory_first (a:S)
+    : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj x a) :=
+    { fmor := fun x y f => PreMonoidalSubCategory_first_fmor a f }.
+    unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+    apply (fmor_respects (-⋉x)); auto.
+    unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0;  simpl in *.
+    apply (fmor_preserves_id (-⋉x)); auto.
+    unfold PreMonoidalSubCategory_first_fmor; intros;
+      destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+    apply (fmor_preserves_comp (-⋉x)); auto.
+    Defined.
+
+  Instance PreMonoidalSubCategory_second (a:S)
+    : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj a x) :=
+    { fmor := fun x y f => PreMonoidalSubCategory_second_fmor a f }.
+    unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+    apply (fmor_respects (x⋊-)); auto.
+    unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0;  simpl in *.
+    apply (fmor_preserves_id (x⋊-)); auto.
+    unfold PreMonoidalSubCategory_second_fmor; intros;
+      destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+    apply (fmor_preserves_comp (x⋊-)); auto.
+    Defined.
+
+  Instance PreMonoidalSubCategory_is_Binoidal : BinoidalCat S PreMonoidalSubCategory_bobj :=
+    { bin_first := PreMonoidalSubCategory_first
+    ; bin_second := PreMonoidalSubCategory_second }.
+
+  Definition PreMonoidalSubCategory_assoc
+    : forall a b,
+      (PreMonoidalSubCategory_second a >>>> PreMonoidalSubCategory_first b) <~~~>
+      (PreMonoidalSubCategory_first  b >>>> PreMonoidalSubCategory_second a).
+    admit.
+    Defined.
+
+  Definition PreMonoidalSubCategory_assoc_ll
+    : forall a b,
+      PreMonoidalSubCategory_second (a⊗b) <~~~>
+      PreMonoidalSubCategory_second b >>>> PreMonoidalSubCategory_second a.
+    intros.
+    admit.
+    Defined.
+
+  Definition PreMonoidalSubCategory_assoc_rr
+    : forall a b,
+      PreMonoidalSubCategory_first (a⊗b) <~~~>
+      PreMonoidalSubCategory_first a >>>> PreMonoidalSubCategory_first b.
+    intros.
+    admit.
+    Defined.
+
+  Definition PreMonoidalSubCategory_I := existT _ pmI (Pobj_unit).
+
+  Definition PreMonoidalSubCategory_cancelr : PreMonoidalSubCategory_first PreMonoidalSubCategory_I <~~~> functor_id _.
+    admit.
+    Defined.
+
+  Definition PreMonoidalSubCategory_cancell : PreMonoidalSubCategory_second PreMonoidalSubCategory_I <~~~> functor_id _.
+    admit.
+    Defined.
+
+  Instance PreMonoidalSubCategory_PreMonoidal : PreMonoidalCat PreMonoidalSubCategory_is_Binoidal PreMonoidalSubCategory_I :=
+  { pmon_assoc           := PreMonoidalSubCategory_assoc 
+  ; pmon_assoc_rr        := PreMonoidalSubCategory_assoc_rr
+  ; pmon_assoc_ll        := PreMonoidalSubCategory_assoc_ll
+  ; pmon_cancelr         := PreMonoidalSubCategory_cancelr
+  ; pmon_cancell         := PreMonoidalSubCategory_cancell
+  }.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  Defined.
+
+End PreMonoidalSubCategory.
diff --git a/src/PreMonoidalCenter.v b/src/PreMonoidalCenter.v
index 61b9372..eb7f608 100644
--- a/src/PreMonoidalCenter.v
+++ b/src/PreMonoidalCenter.v
@@ -3,7 +3,6 @@ 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.
@@ -11,7 +10,7 @@ Require Import NaturalIsomorphisms_ch7_5.
 Require Import Coherence_ch7_8.
 Require Import BinoidalCategories.
 Require Import PreMonoidalCategories.
-Require Import MonoidalCategories_ch_7_8.
+Require Import MonoidalCategories_ch7_8.
 
 (******************************************************************************)
 (* Facts about the center of a Binoidal or PreMonoidal Category               *)
@@ -79,7 +78,7 @@ Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : Ce
   setoid_rewrite pmon_coherent_l at 1.
   setoid_rewrite juggle3.
   setoid_rewrite juggle3.
-  set (@iso_comp2 _ _ _ _ _ ((pmon_assoc C b c0) c)) as q.
+  set (@iso_comp2 _ _ _ _ _ ((pmon_assoc b c0) c)) as q.
   setoid_rewrite q.
   clear q.
   setoid_rewrite right_identity.
@@ -130,7 +129,7 @@ Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : Ce
   setoid_rewrite q.
   clear q.
   
-  set (ni_commutes (pmon_assoc _ d c) f) as q.
+  set (ni_commutes (pmon_assoc d c) f) as q.
   apply iso_shift_right' in q.
   unfold fmor in q at 1; simpl in q.
   rewrite q.
@@ -144,7 +143,9 @@ Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : Ce
   clear q.
 
   setoid_rewrite juggle3.
-  setoid_rewrite (iso_comp1 ((pmon_assoc C d c) a)).
+  set (iso_comp1 ((pmon_assoc d c) a)) as q.
+  setoid_rewrite q.
+  clear q.
   setoid_rewrite right_identity.
 
   set (ni_commutes (pmon_assoc_rr b c) g) as q.
@@ -155,7 +156,7 @@ Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : Ce
   setoid_rewrite q.
   clear q.
   
-  set (ni_commutes (pmon_assoc _ c0 c) f) as q.
+  set (ni_commutes (pmon_assoc c0 c) f) as q.
   unfold fmor in q; simpl in q.
   apply iso_shift_right' in q.
   rewrite q.
@@ -167,7 +168,9 @@ Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : Ce
 
   setoid_rewrite juggle3.
   setoid_rewrite juggle3.
-  setoid_rewrite (iso_comp1 ((pmon_assoc C c0 c) b)).
+  set (iso_comp1 ((pmon_assoc c0 c) b)) as q.
+  setoid_rewrite q.
+  clear q.
   setoid_rewrite right_identity.
 
   setoid_rewrite pmon_coherent_r.
@@ -197,7 +200,7 @@ Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : C
   setoid_rewrite q.
   clear q.
   
-  set (ni_commutes (pmon_assoc _ c d) f) as q.
+  set (ni_commutes (pmon_assoc c d) f) as q.
   apply symmetry in q.
   apply iso_shift_left' in q.
   unfold fmor in q at 1; simpl in q.
@@ -219,7 +222,7 @@ Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : C
   setoid_rewrite q.
   clear q.
   
-  set (ni_commutes (pmon_assoc _ c c0) f) as q.
+  set (ni_commutes (pmon_assoc c c0) f) as q.
   unfold fmor in q; simpl in q.
   symmetry in q.
   apply iso_shift_left' in q.
@@ -229,7 +232,7 @@ Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : C
   rewrite pmon_coherent_l.
   setoid_rewrite <- associativity.
   setoid_rewrite juggle3.
-  set (iso_comp2 ((pmon_assoc _ c c0) b)) as q.
+  set (iso_comp2 ((pmon_assoc c c0) b)) as q.
   setoid_rewrite q.
   setoid_rewrite right_identity.
   clear q.
@@ -302,116 +305,42 @@ Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : C
   setoid_rewrite <- associativity.
   setoid_rewrite juggle3.
   setoid_rewrite pmon_coherent_r.
-  set (iso_comp1 ((pmon_assoc C c0 b) c)) as x.
+  set (iso_comp1 ((pmon_assoc c0 b) c)) as x.
   setoid_rewrite x.
   clear x.
   setoid_rewrite right_identity.
   reflexivity.
   Qed.
 
-Section CenterMonoidal.
+Section Center_is_Monoidal.
 
-  Context `(mc:PreMonoidalCat(I:=pI)).
+  Context `(pm:PreMonoidalCat(I:=pmI)).
 
-  Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc.
-    intro.
-    destruct X as [a b].
-    destruct a as [a apf].
-    destruct b as [b bpf].
-    exists (a ⊗ b); auto.
+  Definition Center_bobj : Center pm -> Center pm -> Center pm.
+    apply PreMonoidalSubCategory_bobj.
+    intros; auto.
     Defined.
 
-  Definition CenterMonoidal_F_fmor (a b:(Center mc) ×× (Center mc)) : 
-    (a~~{(Center mc) ×× (Center mc)}~~>b) ->
-    ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)).
-    destruct a as [[a1 a1'] [a2 a2']].
-    destruct b as [[b1 b1'] [b2 b2']].
-    intro f.
-    destruct f as [[f1 f1'] [f2 f2']].
-    simpl in *.
-    unfold hom.
-    simpl.
-    exists (f1 ⋉ a2 >>> b1 ⋊ f2).
-    apply central_morphisms_compose.
-    apply first_preserves_centrality; auto.
-    apply second_preserves_centrality; auto.
-    Defined.
-
-  Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
-    refine {| fmor := CenterMonoidal_F_fmor |}.
-    intros.
-    destruct a as [[a1 a1'] [a2 a2']].
-    destruct b as [[b1 b1'] [b2 b2']].
-    destruct f as [[f1 f1'] [f2 f2']].
-    destruct f' as [[g1 g1'] [g2 g2']].
-    simpl in *.
-    destruct H.
-    apply comp_respects.
-    set (fmor_respects(-⋉a2)) as q; apply q; auto.
-    set (fmor_respects(b1⋊-)) as q; apply q; auto.
+  Definition Center_is_Binoidal : BinoidalCat (Center pm) Center_bobj.
+    apply PreMonoidalSubCategory_is_Binoidal.
     intros.
-    destruct a as [[a1 a1'] [a2 a2']].
-    simpl in *.
-    setoid_rewrite (fmor_preserves_id (-⋉a2)).
-    setoid_rewrite (fmor_preserves_id (a1⋊-)).
-    apply left_identity.
+    apply first_preserves_centrality; auto.
     intros.
-    destruct a as [[a1 a1'] [a2 a2']].
-    destruct b as [[b1 b1'] [b2 b2']].
-    destruct c as [[c1 c1'] [c2 c2']].
-    destruct f as [[f1 f1'] [f2 f2']].
-    destruct g as [[g1 g1'] [g2 g2']].
-    simpl in *.
-    setoid_rewrite juggle3.
-    setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
-    setoid_rewrite <- juggle3.
-    setoid_rewrite <- fmor_preserves_comp.
-    reflexivity.
-    Defined.
-
-  Definition center_I : Center mc := exist _ pI I.
-
-  Definition center_cancelr : (func_rlecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc).
-    Definition center_cancelr_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj A center_I) ≅ A.
-      intros.
-      destruct A; simpl.
-      set (ni_iso (pmon_cancelr mc) x) as q.
-      (*refine {| iso_forward := #q ; iso_backward := iso_backward q |}.*)
-      admit.
-      Defined.
-    refine {| ni_iso := center_cancelr_niso |}.
-    admit.
-    Defined.
-
-  Definition center_cancell : (func_llecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc).
-    Definition center_cancell_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj center_I A) ≅ A.
-      admit.
-      Defined.
-    refine {| ni_iso := center_cancell_niso |}.
-    admit.
+    apply second_preserves_centrality; auto.
     Defined.
 
-  Definition center_assoc :
-    ((CenterMonoidal_F **** (functor_id _)) >>>> CenterMonoidal_F)
-    <~~~> func_cossa >>>> ((((functor_id _) **** CenterMonoidal_F) >>>> CenterMonoidal_F)).
-
-    Definition center_assoc_niso : ∀A : (Center mc ×× Center mc) ×× Center mc,
-      ((((CenterMonoidal_F **** (functor_id _)) >>>> CenterMonoidal_F) A))
-      ≅ ((func_cossa >>>> ((((functor_id _) **** CenterMonoidal_F) >>>> CenterMonoidal_F))) A).
-      admit.
-      Defined.
-
-    refine {| ni_iso := center_assoc_niso |}.
-    admit.
+  Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal (exist _ pmI I).
+    apply PreMonoidalSubCategory_PreMonoidal.
     Defined.
 
-  Instance CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I) :=
-  { mon_cancelr := center_cancelr
-  ; mon_cancell := center_cancell
-  ; mon_assoc   := center_assoc
-  }.
-    admit.
-    admit.
+  Definition Center_is_Monoidal : MonoidalCat Center_is_PreMonoidal.
+    apply Build_MonoidalCat.
+    apply Build_CommutativeCat.
+    intros.
+    apply Build_CentralMorphism; unfold hom; 
+      intros; destruct f; destruct a; destruct c; destruct d; destruct b; destruct g; simpl in *.
+    apply centralmor_second.
+    apply centralmor_second.
     Defined.
 
-End CenterMonoidal.
+End Center_is_Monoidal.
diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v
index f318c7c..2cfe5eb 100644
--- a/src/RepresentableStructure_ch7_2.v
+++ b/src/RepresentableStructure_ch7_2.v
@@ -23,8 +23,8 @@ Require Import MonoidalCategories_ch7_8.
 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.
+  Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
+  Definition hom_covariant     {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr _)⁻¹ >>> ((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).
@@ -97,7 +97,7 @@ Section RepresentableStructure.
       apply fmor_respects; auto.
     intros.
       unfold hom_covariant.
-      apply (epic _ (iso_epic ((pmon_cancelr mn) (X ~~> a)))).
+      apply (epic _ (iso_epic ((pmon_cancelr) (X ~~> a)))).
       setoid_rewrite <- associativity.
       setoid_rewrite <- associativity.
       setoid_rewrite iso_comp1.
@@ -152,45 +152,3 @@ Section RepresentableStructure.
 End RepresentableStructure.
 Opaque HomFunctor.
 
-Structure MonoidalEnrichment {e:Enrichment} :=
-{ me_enr         :=e
-; me_fobj        : prod_obj e e -> e
-; me_f           : Functor (e ×× e) e me_fobj
-; me_i           : e
-; me_mon         : MonoidalCat e me_fobj me_f me_i
-; me_mf          : MonoidalFunctor me_mon (enr_v_mon e) (HomFunctor e me_i)
-}.
-Implicit Arguments MonoidalEnrichment [ ].
-Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
-Coercion me_enr : MonoidalEnrichment >-> Enrichment.
-
-(* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
-Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} :=
-{ ffme_enr             := me
-; ffme_mf_full         : FullFunctor         (HomFunctor e (me_i me))
-; ffme_mf_faithful     : FaithfulFunctor     (HomFunctor e (me_i me))
-; ffme_mf_conservative : ConservativeFunctor (HomFunctor e (me_i me))
-}.
-Implicit Arguments MonicMonoidalEnrichment [ ].
-Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
-Transparent HomFunctor.
-
-Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) :=
-{ smme_se       : SurjectiveEnrichment e
-; smme_monoidal : MonoidalEnrichment e
-; smme_me       : MonicMonoidalEnrichment _ smme_monoidal
-}.
-Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment.
-Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment.
-
-(* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
-Structure SMME :=
-{ smme_e   : Enrichment
-; smme_see : SurjectiveEnrichment smme_e
-; smme_mon : MonoidalEnrichment smme_e
-; smme_mee : MonicMonoidalEnrichment _ smme_mon
-}.
-Coercion smme_e   : SMME >-> Enrichment.
-Coercion smme_see : SMME >-> SurjectiveEnrichment.
-Coercion smme_mon : SMME >-> MonoidalEnrichment.
-Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.
diff --git a/src/SectionRetract_ch2_4.v b/src/SectionRetract_ch2_4.v
index 3eda753..2d4f859 100644
--- a/src/SectionRetract_ch2_4.v
+++ b/src/SectionRetract_ch2_4.v
@@ -4,6 +4,7 @@ Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
 Require Import ProductCategories_ch1_6_1.
+Require Import NaturalIsomorphisms_ch7_5.
 
 (******************************************************************************)
 (* Chapter 2.4: Sections and Retractions                                      *)
@@ -54,3 +55,13 @@ Instance retract_prod `{C:Category}`{D:Category}{a b:C}{d e:D}(r1:a ⊆ b)(r2:d
 }.
   simpl; split; apply retract_pf.
   Defined.
+
+Structure Retraction `{C:Category} `{D:Category} :=
+{ retraction_section_fobj       : C -> D
+; retraction_section            : Functor C D retraction_section_fobj
+; retraction_retraction_fobj    : D -> C
+; retraction_retraction         : Functor D C retraction_retraction_fobj
+; retraction_composes           : retraction_section >>>> retraction_retraction ≃ functor_id _
+}.
+Implicit Arguments Retraction [ [Ob] [Hom] [Ob0] [Hom0] ].
+Coercion retraction_section : Retraction >-> Functor.
diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v
index e6b8aa4..78bf98f 100644
--- a/src/Subcategories_ch7_1.v
+++ b/src/Subcategories_ch7_1.v
@@ -94,7 +94,7 @@ Section RestrictToImage.
     Qed.
 End RestrictToImage.
 
-Instance func_opSubcat `(c1:Category Ob1 Hom1)`(c2:Category Ob Hom)`(SP:@SubCategory _ _ c2 Pobj Pmor)
+Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor)
   {fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=
   { fmor                := fun a b f => fmor F f }.
   intros. apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H).
@@ -190,7 +190,7 @@ Definition WeaklyMonic
     `{D:Category}
      {Fobj}
      (F:@Functor _ _ C _ _ D Fobj) := forall
-    `{E:Category}
+     Eob EHom (E:@Category Eob EHom)
     `{G :@Functor _ _ E _ _ C Gobj'}
     `{H :@Functor _ _ E _ _ C Hobj'},
     G >>>> F ≃ H >>>> F