Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried


Require Import UniMath.Foundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.

Local Open Scope cat.

Data

  Definition tensor_data (C : category) : UU :=
     to : C -> C -> C,
             (x y x' y' : C), C x,x' C y,y' -> C ⟦(to x y),(to x' y')⟧.

  Definition tensoronobjects_from_tensordata {C : category} (T : tensor_data C) : C->C->C := pr1 T.
  Notation "x ⊗_{ T } y" := (tensoronobjects_from_tensordata T x y) (at level 31).

  Definition tensoronmorphisms_from_tensordata {C : category} (T : tensor_data C):
     (x y x' y' : C), C x,x' C y,y' -> C x _{T} y,x' _{T} y'
    := pr2 T.
  Notation "f ⊗^{ T } g" := (tensoronmorphisms_from_tensordata T _ _ _ _ f g) (at level 31).

  Definition associator_data {C : category} (T : tensor_data C) : UU :=
     (x y z : C), C (x _{T} y) _{T} z, x _{T} (y _{T} z).

  Definition leftunitor_data {C : category} (T : tensor_data C) (I : C) : UU :=
     (x : C), C I _{T} x, x.

  Definition rightunitor_data {C : category} (T : tensor_data C) (I : C) : UU :=
     (x : C), C x _{T} I, x.

  Definition monoidalcategory_data (C : category): UU :=
     T : tensor_data C, I : C,
          (leftunitor_data T I) × (rightunitor_data T I) × (associator_data T).

Definition tensordata_from_monoidalcatdata {C : category} (MD : monoidalcategory_data C) : tensor_data C := (pr1 MD).
Coercion tensordata_from_monoidalcatdata : monoidalcategory_data >-> tensor_data.

Definition unit_from_monoidalcatdata {C : category} (MD : monoidalcategory_data C) : C := (pr1 (pr2 MD)).
Coercion unit_from_monoidalcatdata : monoidalcategory_data >-> ob.

Definition leftunitordata_from_monoidalcatdata {C : category} (MD : monoidalcategory_data C) : leftunitor_data MD MD := (pr1 (pr2 (pr2 MD))).
Coercion leftunitordata_from_monoidalcatdata : monoidalcategory_data >-> leftunitor_data.

Definition rightunitordata_from_monoidalcatdata {C : category} (MD : monoidalcategory_data C) : rightunitor_data MD MD := (pr1 (pr2 (pr2 (pr2 MD)))).
Coercion rightunitordata_from_monoidalcatdata : monoidalcategory_data >-> rightunitor_data.

Definition associatordata_from_monoidalcatdata {C : category} (MD : monoidalcategory_data C) : associator_data MD := (pr2 (pr2 (pr2 (pr2 MD)))).
Coercion associatordata_from_monoidalcatdata : monoidalcategory_data >-> associator_data.

Axioms
  Definition tensorfunctor_id {C : category} (T : tensor_data C) : UU :=
     (x y : C),
      (identity x) ⊗^{T} identity y = identity (x _{T} y).

  Definition tensorfunctor_comp {C : category} (T : tensor_data C) : UU :=
     (x y x' y' x'' y'' : C), (f : C x,x') (f' : C x',x'') (g : C y,y') (g' : C y',y''),
      (f' ⊗^{T} g') (f ⊗^{T} g) = (f'f) ⊗^{T} (g'g).

  Definition associator_naturality {C : category} {T : tensor_data C} (α : associator_data T) : UU :=
     (x x' y y' z z' : C), (f : Cx,x') (g : Cy,y') (h : Cz,z'),
       (f ⊗^{T} (g ⊗^{T} h))∘(α x y z) = (α x' y' z')∘ ((f ⊗^{T} g) ⊗^{T} h).

  Definition associator_is_natiso {C : category} {T : tensor_data C} (α : associator_data T) : UU :=
     (x y z : C), is_z_isomorphism (α x y z).

  Definition leftunitor_naturality {C : category} {T : tensor_data C} {I : C} (lu : leftunitor_data T I) : UU :=
     (x y : C), (f : C x,y), f∘(lu x) = (lu y)∘((identity I)⊗^{T}f).

  Definition leftunitor_is_natiso {C : category} {T : tensor_data C} {I : C} (lu : leftunitor_data T I) : UU :=
     (x : C), is_z_isomorphism (lu x).

  Definition rightunitor_naturality {C : category} {T : tensor_data C} {I : C} (ru : rightunitor_data T I) :=
     (x y : C), (f : C x,y), f∘(ru x) = (ru y)∘ (f ⊗^{T} (identity I)).

  Definition rightunitor_is_natiso {C : category} {T : tensor_data C} {I : C} (ru : rightunitor_data T I) : UU :=
     (x : C), is_z_isomorphism (ru x).

  Definition triangle_identity {C : category}
             {T : tensor_data C}
             {I : C}
             (lu : leftunitor_data T I)
             (ru : rightunitor_data T I)
             (α : associator_data T)
    := (x y : C), (((identity x) ⊗^{T} (lu y) ) (α x I y)) = ((ru x) ⊗^{T} identity y).

  Definition pentagon_identity {C : category} {T : tensor_data C} (α : associator_data T) : UU :=
     (w x y z : C),
         ((identity w)⊗^{T} (α x y z))
            ((α w (x_{T} y) z)
            ((α w x y) ⊗^{T} (identity z))) = (α w x (y_{T} z)) (α (w_{T}x) y z).

Definition monoidal_laws {C : category} (MD : monoidalcategory_data C) : UU :=
  (tensorfunctor_id MD) × (tensorfunctor_comp MD) × (associator_naturality MD) × (associator_is_natiso MD) ×
                                                    (leftunitor_naturality MD) × (leftunitor_is_natiso MD) ×
                                                    (rightunitor_naturality MD) × (rightunitor_is_natiso MD) ×
                                                    (triangle_identity MD MD MD) × (pentagon_identity MD).

Definition tensorfunctorialityid_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : tensorfunctor_id MD := pr1 ML.
Coercion tensorfunctorialityid_from_monoidallaws : monoidal_laws >-> tensorfunctor_id.

Definition tensorfunctorialitycomp_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : tensorfunctor_comp MD := pr1 (pr2 ML).
Coercion tensorfunctorialitycomp_from_monoidallaws : monoidal_laws >-> tensorfunctor_comp.

Definition associatornaturality_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : associator_naturality MD := pr1 (pr2 (pr2 ML)).
Coercion associatornaturality_from_monoidallaws : monoidal_laws >-> associator_naturality.

Definition associatorisiso_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : associator_is_natiso MD := pr1 (pr2 (pr2 (pr2 ML))).
Coercion associatorisiso_from_monoidallaws : monoidal_laws >-> associator_is_natiso.

Definition leftunitornaturality_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : leftunitor_naturality MD := pr1 (pr2 (pr2 (pr2 (pr2 ML)))).
Coercion leftunitornaturality_from_monoidallaws : monoidal_laws >-> leftunitor_naturality.

Definition leftunitorisiso_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : leftunitor_is_natiso MD := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 ML))))).
Coercion leftunitorisiso_from_monoidallaws : monoidal_laws >-> leftunitor_is_natiso.

Definition rightunitornaturality_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : rightunitor_naturality MD := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 ML)))))).
Coercion rightunitornaturality_from_monoidallaws : monoidal_laws >-> rightunitor_naturality.

Definition rightunitorisiso_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : rightunitor_is_natiso MD := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 ML))))))).
Coercion rightunitorisiso_from_monoidallaws : monoidal_laws >-> rightunitor_is_natiso.

Definition triangleidentity_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : triangle_identity MD MD MD := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 ML)))))))).
Coercion triangleidentity_from_monoidallaws : monoidal_laws >-> triangle_identity.

Definition pentagonidentity_from_monoidallaws {C : category} {MD : monoidalcategory_data C} (ML : monoidal_laws MD) : pentagon_identity MD := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 ML)))))))).
Coercion pentagonidentity_from_monoidallaws : monoidal_laws >-> pentagon_identity.

Definition monoidalcategory (C : category) : UU :=
   (MD : monoidalcategory_data C), (monoidal_laws MD).

Definition monoidalcategorydata_from_monoidalcategory {C : category} (M : monoidalcategory C) : monoidalcategory_data C := pr1 M.
Coercion monoidalcategorydata_from_monoidalcategory : monoidalcategory >-> monoidalcategory_data.

Definition monoidallaws_from_monoidalcategory {C : category} (M : monoidalcategory C) : monoidal_laws M := pr2 M.
Coercion monoidallaws_from_monoidalcategory : monoidalcategory >-> monoidal_laws.