add MonoidalNaturalIsomorphism, MonoidalEquivalence, MonoidalNaturalEquivalence

[coq-categories.git] / src / MonoidalCategories_ch7_8.v

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index e9d3799..9033f4c 100644 (file)
--- a/src/MonoidalCategories_ch7_8.v
+++ b/src/MonoidalCategories_ch7_8.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
 Generalizable All Variables.

-Require Import Preamble.
+Require Import Notations.

 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

@@ -32,21 +32,59 @@ 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 *)
 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
 
 Definition MonoidalFunctorsCompose

-  `{M1   :MonoidalCat(C:=C1)}
-  `{M2   :MonoidalCat(C:=C2)}
+  `{PM1   :MonoidalCat(C:=C1)}
+  `{PM2   :MonoidalCat(C:=C2)}

    {fobj12:C1 -> 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                    }
    {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).
 
 Section BinoidalCat_from_Bifunctor.
   Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).

@@ -148,13 +186,12 @@ Class DiagonalCat `(mc:MonoidalCat) :=
 }.
 
 Class CartesianCat `(mc:MonoidalCat) :=
 }.
 
 Class CartesianCat `(mc:MonoidalCat) :=

-{ car_terminal  :> Terminal mc
-; car_one       :  one ≅ pmon_I
+{ car_terminal  :> TerminalObject mc pmon_I

 ; car_diagonal  :  DiagonalCat 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.
 ; car_mn        := mc
 }.
 Coercion car_diagonal : CartesianCat >-> DiagonalCat.

-Coercion car_terminal : CartesianCat >-> Terminal.
+Coercion car_terminal : CartesianCat >-> TerminalObject.

 Coercion car_mn       : CartesianCat >-> MonoidalCat.
 Coercion car_mn       : CartesianCat >-> MonoidalCat.