--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import Subcategories_ch7_1.
+
+(******************************************************************************)
+(* Binoidal Categories (not in Awodey) *)
+(******************************************************************************)
+
+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 ⋉ _)
+}.
+
+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.
+ 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.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
Require Import MonoidalCategories_ch7_8.
(******************************************************************************)
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
(******************************************************************************)
-(* Chapter 7.8: (Pre)Monoidal Categories *)
+(* Chapter 7.8: 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 ⋉ _)
-}.
-
-Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
- : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
- intros.
- apply Build_CentralMorphism; intros.
- 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.
-
-(* 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).
- apply central_morphisms_compose; auto.
- 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.
- 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.
-
-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_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
-}.
-
-Class SymmetricCat `(bc:BraidedCat) :=
-{ symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
-}.
-
-(* 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
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).
+
+ 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.
+ 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.
+ Defined.
+
+End MonoidalFunctorsCompose.
+
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.
(* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
}.
-(* 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).
-
- 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.
- 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.
- Defined.
-
-End MonoidalFunctorsCompose.
-
Class CartesianCat `(mc:MonoidalCat) :=
{ car_terminal : Terminal mc
; car_one : (@one _ _ _ car_terminal) ≅ (mon_i mc)
Coercion car_diagonal : CartesianCat >-> DiagonalCat.
Coercion car_terminal : CartesianCat >-> Terminal.
Coercion car_mn : CartesianCat >-> MonoidalCat.
-
-Section CenterMonoidal.
-
- Context `(mc:PreMonoidalCat(I:=pI)).
-
- 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.
- 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.
- admit.
- admit.
- 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.
- 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.
- 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 CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I).
- admit.
- Defined.
-
-End CenterMonoidal.
-
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import InitialTerminal_ch2_2.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import Coherence_ch7_8.
+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)
+}.
+(*
+ * 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.
+
+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_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
+}.
+
+Class SymmetricCat `(bc:BraidedCat) :=
+{ symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
+}.
--- /dev/null
+Generalizable All Variables.
+Require Import Preamble.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import InitialTerminal_ch2_2.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
+Require Import MonoidalCategories_ch_7_8.
+
+(******************************************************************************)
+(* Facts about the center of a Binoidal or PreMonoidal Category *)
+(******************************************************************************)
+
+Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
+ : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
+ intros.
+ apply Build_CentralMorphism; intros.
+ 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.
+
+(* 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).
+ apply central_morphisms_compose; auto.
+ Qed.
+
+
+Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c).
+ intro cm.
+ apply Build_CentralMorphism; simpl; intros.
+
+ set (ni_commutes (pmon_assoc_rr c c0) f) as q.
+ apply iso_shift_right' in q.
+ unfold fmor in q at 1; simpl in q.
+ rewrite q.
+ clear q.
+
+ set (ni_commutes (pmon_assoc_rr c d) f) as q.
+ apply iso_shift_right' in q.
+ unfold fmor in q at 1; simpl in q.
+ rewrite q.
+ clear q.
+
+ set (ni_commutes (pmon_assoc_ll b c) g) as q.
+ apply symmetry in q.
+ apply iso_shift_left' in q.
+ rewrite q.
+ clear q.
+
+ setoid_rewrite pmon_coherent_r at 1.
+ setoid_rewrite pmon_coherent_l at 1.
+ setoid_rewrite juggle3.
+ setoid_rewrite juggle3.
+ set (@iso_comp2 _ _ _ _ _ ((pmon_assoc C b c0) c)) as q.
+ setoid_rewrite q.
+ clear q.
+ setoid_rewrite right_identity.
+ unfold fmor at 2.
+ simpl.
+ setoid_rewrite (centralmor_first(CentralMorphism:=cm)).
+
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects.
+ apply comp_respects; [ idtac | reflexivity ].
+ set (ni_commutes (pmon_assoc_ll a c) g) as q.
+ apply symmetry in q.
+ apply iso_shift_left' in q.
+ setoid_rewrite q.
+ clear q.
+ repeat setoid_rewrite associativity.
+ setoid_rewrite pmon_coherent_l.
+ set (pmon_coherent_l(PreMonoidalCat:=C) c a d) as q.
+ apply isos_forward_equal_then_backward_equal in q.
+ setoid_rewrite q.
+ clear q.
+ setoid_rewrite <- pmon_coherent_r.
+ setoid_rewrite iso_comp1.
+ setoid_rewrite right_identity.
+ unfold fmor at 3; simpl.
+ apply comp_respects; [ idtac | reflexivity ].
+
+ set (pmon_coherent_r a c c0) as q.
+ apply isos_forward_equal_then_backward_equal in q.
+ setoid_rewrite iso_inv_inv in q.
+ apply q.
+
+ setoid_rewrite pmon_coherent_r.
+ unfold iso_inv.
+ simpl.
+ set (@isos_forward_equal_then_backward_equal) as q.
+ unfold iso_inv in q; simpl in q.
+ apply q.
+ apply pmon_coherent_l.
+
+ (* *)
+
+ set (ni_commutes (pmon_assoc_rr a c) g) as q.
+ symmetry in q.
+ apply iso_shift_left' in q.
+ unfold fmor in q at 2.
+ simpl in q.
+ setoid_rewrite q.
+ clear 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.
+ clear q.
+
+ set (pmon_coherent_r d a c) as q.
+ apply isos_forward_equal_then_backward_equal in q.
+ rewrite iso_inv_inv in q.
+ unfold iso_inv in q; simpl in q.
+ rewrite q.
+ clear q.
+
+ setoid_rewrite juggle3.
+ setoid_rewrite (iso_comp1 ((pmon_assoc C d c) a)).
+ setoid_rewrite right_identity.
+
+ set (ni_commutes (pmon_assoc_rr b c) g) as q.
+ symmetry in q.
+ apply iso_shift_left' in q.
+ unfold fmor in q at 2.
+ simpl in q.
+ setoid_rewrite q.
+ clear 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.
+ clear q.
+
+ set (pmon_coherent_r c0 b c) as q.
+ rewrite q.
+ clear q.
+
+ setoid_rewrite juggle3.
+ setoid_rewrite juggle3.
+ setoid_rewrite (iso_comp1 ((pmon_assoc C c0 c) b)).
+ setoid_rewrite right_identity.
+
+ setoid_rewrite pmon_coherent_r.
+ repeat setoid_rewrite associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects.
+ setoid_rewrite (fmor_preserves_comp (-⋉c)).
+ apply (fmor_respects (-⋉c)).
+ apply centralmor_second.
+ set (pmon_coherent_r d b c) as q.
+ apply isos_forward_equal_then_backward_equal in q.
+ rewrite iso_inv_inv in q.
+ symmetry.
+ apply q.
+ Qed.
+
+Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (c ⋊ f).
+ intro cm.
+ apply Build_CentralMorphism; simpl; intros.
+
+ set (ni_commutes (pmon_assoc_ll c a) g) as q.
+ symmetry in q.
+ apply iso_shift_left' in q.
+ unfold fmor in q at 2.
+ simpl in q.
+ setoid_rewrite q.
+ clear 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.
+ rewrite q.
+ clear q.
+
+ rewrite <- pmon_coherent_l.
+ setoid_rewrite <- associativity.
+ setoid_rewrite juggle3.
+ set (iso_comp2 ((pmon_assoc_ll c a) d)) as q.
+ setoid_rewrite q.
+ setoid_rewrite right_identity.
+ clear q.
+
+ set (ni_commutes (pmon_assoc_ll c b) g) as q.
+ apply symmetry in q.
+ apply iso_shift_left' in q.
+ unfold fmor in q at 1; simpl in q.
+ setoid_rewrite q.
+ clear 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.
+ rewrite q.
+ clear q.
+
+ rewrite pmon_coherent_l.
+ setoid_rewrite <- associativity.
+ setoid_rewrite juggle3.
+ set (iso_comp2 ((pmon_assoc _ c c0) b)) as q.
+ setoid_rewrite q.
+ setoid_rewrite right_identity.
+ clear q.
+ setoid_rewrite pmon_coherent_l.
+
+ repeat setoid_rewrite associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ repeat setoid_rewrite <- associativity.
+ apply comp_respects.
+ setoid_rewrite (fmor_preserves_comp (c⋊-)).
+ apply (fmor_respects (c⋊-)).
+ apply centralmor_first.
+ set (pmon_coherent_l b c d) as q.
+ apply isos_forward_equal_then_backward_equal in q.
+ apply q.
+
+ (* *)
+ set (ni_commutes (pmon_assoc_ll d c) f) as q.
+ apply iso_shift_right' in q.
+ unfold fmor in q at 1; simpl in q.
+ rewrite q.
+ clear q.
+
+ set (ni_commutes (pmon_assoc_rr c a) g) as q.
+ apply symmetry in q.
+ unfold fmor in q at 2; simpl in q.
+ apply iso_shift_left' in q.
+ rewrite q.
+ clear q.
+
+ setoid_rewrite juggle3.
+ set (pmon_coherent_r d c a) as q.
+ apply isos_forward_equal_then_backward_equal in q.
+ setoid_rewrite iso_inv_inv in q.
+ setoid_rewrite q.
+ clear q.
+ setoid_rewrite <- pmon_coherent_l.
+ set (iso_comp1 (((pmon_assoc_ll d c) a))) as q.
+ setoid_rewrite q.
+ clear q.
+ setoid_rewrite right_identity.
+ setoid_rewrite juggle3.
+ setoid_rewrite (centralmor_second(CentralMorphism:=cm)).
+ symmetry.
+ apply iso_shift_left.
+ setoid_rewrite pmon_coherent_r.
+ set (pmon_coherent_l c d b) as q.
+ apply isos_forward_equal_then_backward_equal in q.
+ setoid_rewrite q.
+ clear q.
+ apply iso_shift_right.
+ setoid_rewrite iso_inv_inv.
+ repeat setoid_rewrite <- associativity.
+
+ set (ni_commutes (pmon_assoc_ll c0 c) f) as x.
+ setoid_rewrite <- pmon_coherent_l.
+ symmetry in x.
+ unfold fmor in x at 2; simpl in x.
+ setoid_rewrite <- x.
+ clear x.
+
+ set (ni_commutes (pmon_assoc_rr c b) g) as x.
+ symmetry in x.
+ unfold fmor in x at 2; simpl in x.
+ setoid_rewrite pmon_coherent_l.
+ setoid_rewrite <- pmon_coherent_r.
+ repeat setoid_rewrite associativity.
+ setoid_rewrite x.
+ clear x.
+ setoid_rewrite <- associativity.
+ setoid_rewrite juggle3.
+ setoid_rewrite pmon_coherent_r.
+ set (iso_comp1 ((pmon_assoc C c0 b) c)) as x.
+ setoid_rewrite x.
+ clear x.
+ setoid_rewrite right_identity.
+ reflexivity.
+ Qed.
+
+Section CenterMonoidal.
+
+ Context `(mc:PreMonoidalCat(I:=pI)).
+
+ 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.
+ 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.
+ 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.
+ 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.
+ 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.
+ Defined.
+
+ Instance CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I) :=
+ { mon_cancelr := center_cancelr
+ ; mon_cancell := center_cancell
+ ; mon_assoc := center_assoc
+ }.
+ admit.
+ admit.
+ Defined.
+
+End CenterMonoidal.
Require Import NaturalIsomorphisms_ch7_5.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
+Require Import MonoidalCategories_ch7_8.
Section RepresentableStructure.
Context `(ec:ECategory(mn:=mn)(V:=V)).