-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 *)