Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
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 MonoidalFunctor `(m1:MonoidalCat) `(m2:MonoidalCat) {fobj}(F:Functor m1 m2 fobj) := PreMonoidalFunctor m1 m2 F.
Definition MonoidalFunctorsCompose
- `{M1 :MonoidalCat(C:=C1)}
- `{M2 :MonoidalCat(C:=C2)}
+ `{PM1 :MonoidalCat(C:=C1)}
+ `{PM2 :MonoidalCat(C:=C2)}
{fobj12:C1 -> C2 }
- (MF12 :MonoidalFunctor M1 M2 fobj12)
- `{M3 :MonoidalCat(C:=C3)}
+ {PMFF12:Functor C1 C2 fobj12 }
+ (PMF12 :MonoidalFunctor PM1 PM2 PMFF12)
+ `{PM3 :MonoidalCat(C:=C3)}
{fobj23:C2 -> C3 }
- (MF23 :MonoidalFunctor M2 M3 fobj23)
- : MonoidalFunctor M1 M3 (fobj23 ○ fobj12).
- apply PreMonoidalFunctorsCompose.
- apply MF12.
- apply MF23.
- Defined.
+ {PMFF23:Functor C2 C3 fobj23 }
+ (PMF23 :MonoidalFunctor PM2 PM3 PMFF23)
+ := PreMonoidalFunctorsCompose PMF12 PMF23.
+
+Class MonoidalNaturalIsomorphism
+ `{C1:MonoidalCat}`{C2:MonoidalCat}
+ `(F1:!MonoidalFunctor(fobj:=fobj1) C1 C2 Func1)
+ `(F2:!MonoidalFunctor(fobj:=fobj2) C1 C2 Func2) :=
+{ mni_ni : NaturalIsomorphism F1 F2
+; mni_commutes1 : forall A B,
+ #(ni_iso (mf_first(PreMonoidalFunctor:=F1) B) A) >>> #(ni_iso mni_ni (A⊗B)) ~~
+ #(ni_iso mni_ni _) ⋉ _ >>> _ ⋊ #(ni_iso mni_ni _) >>> #(ni_iso (mf_first(PreMonoidalFunctor:=F2) B) A)
+; mni_commutes2 : forall A B,
+ #(ni_iso (mf_second(PreMonoidalFunctor:=F1) A) B) >>> #(ni_iso mni_ni (A⊗B)) ~~
+ #(ni_iso mni_ni _) ⋉ _ >>> _ ⋊ #(ni_iso mni_ni _) >>> #(ni_iso (mf_second(PreMonoidalFunctor:=F2) A) B)
+}.
+Notation "F <~~⊗~~> G" := (@MonoidalNaturalIsomorphism _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ F _ _ G) : category_scope.
+
+(* an equivalence of categories via monoidal functors, but the natural iso isn't necessarily a monoidal natural iso *)
+Structure MonoidalEquivalence `{C1:MonoidalCat} `{C2:MonoidalCat} :=
+{ meqv_forward_fobj : C1 -> C2
+; meqv_forward : Functor C1 C2 meqv_forward_fobj
+; meqv_forward_mon : PreMonoidalFunctor _ _ meqv_forward
+; meqv_backward_fobj : C2 -> C1
+; meqv_backward : Functor C2 C1 meqv_backward_fobj
+; meqv_backward_mon : PreMonoidalFunctor _ _ meqv_backward
+; meqv_comp1 : meqv_forward >>>> meqv_backward ≃ functor_id _
+; meqv_comp2 : meqv_backward >>>> meqv_forward ≃ functor_id _
+}.
+
+(* a monoidally-natural equivalence of categories *)
+(*
+Structure MonoidalNaturalEquivalence `{C1:MonoidalCat} `{C2:MonoidalCat} :=
+{ mneqv_forward_fobj : C1 -> C2
+; mneqv_forward : Functor C1 C2 mneqv_forward_fobj
+; mneqv_forward_mon : PreMonoidalFunctor _ _ mneqv_forward
+; mneqv_backward_fobj : C2 -> C1
+; mneqv_backward : Functor C2 C1 mneqv_backward_fobj
+; mneqv_backward_mon : PreMonoidalFunctor _ _ mneqv_backward
+; mneqv_comp1 : mneqv_forward_mon >>⊗>> mneqv_backward_mon <~~⊗~~> premonoidal_id _
+; mneqv_comp2 : mneqv_backward_mon >>⊗>> mneqv_forward_mon <~~⊗~~> premonoidal_id _
+}.
+*)
Section BinoidalCat_from_Bifunctor.
Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
End Bifunctor_from_MonoidalCat.
+Instance MonoidalFullSubcategory_Monoidal `(mc:MonoidalCat) {Pobj} Pobj_unit Pobj_closed V
+ : MonoidalCat (PreMonoidalFullSubcategory_PreMonoidal(Pobj:=Pobj) mc V Pobj_unit Pobj_closed).
+ apply Build_MonoidalCat.
+ apply Build_CommutativeCat.
+ intros.
+ idtac.
+ apply Build_CentralMorphism; intros.
+ destruct a.
+ destruct b.
+ destruct c.
+ destruct d.
+ simpl.
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=mon_commutative(MonoidalCat:=mc)) f)).
+
+ destruct a.
+ destruct b.
+ destruct c.
+ destruct d.
+ simpl.
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=mon_commutative(MonoidalCat:=mc)) g)).
+ Defined.
+
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 _
}.
Class CartesianCat `(mc:MonoidalCat) :=
-{ car_terminal :> Terminal mc
-; car_one : one ≅ pmon_I
+{ car_terminal :> TerminalObject mc (pmon_I mc)
; 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_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (drop a ⋉ a) >>> (#(pmon_cancell _))
+; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ drop a) >>> (#(pmon_cancelr _))
; car_mn := mc
}.
Coercion car_diagonal : CartesianCat >-> DiagonalCat.
-Coercion car_terminal : CartesianCat >-> Terminal.
+Coercion car_terminal : CartesianCat >-> TerminalObject.
Coercion car_mn : CartesianCat >-> MonoidalCat.