Require Import Basics.Utf8.
Require Import Category.Core Category.Morphisms.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Functor.Core
        Functor.Utf8.
Require Import NaturalTransformation.Core.
Require Import FunctorCategory.Core FunctorCategory.Morphisms.
Require Import ProductLaws.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Section MonoidalStructure.
  Context `{Funext}.

Local Notation "x --> y" := (morphism _ x y).

Section MonoidalCategoryConcepts.
  Variable C : PreCategory.
  Variable tensor : ((C * C) -> C)%category.
  Variable I : C.

  Local Notation "A ⊗ B" := (tensor (Basics.Overture.pair A B)).

  Local Open Scope functor_scope.
  Definition right_assoc := (tensor ∘ (Functor.Prod.pair 1 tensor) )%functor.
  Definition left_assoc :=  tensor ∘
                                   (Functor.Prod.pair tensor 1) ∘
                                   (Associativity.functor _ _ _).

  Definition associator := NaturalIsomorphism right_assoc left_assoc.
  (* Orientation  (A ⊗ B) ⊗ C -> A ⊗ (B ⊗ C) *)
  Definition pretensor (A : C) := Core.induced_snd tensor A.
  Definition I_pretensor := pretensor I.
  Definition posttensor (A : C) := Core.induced_fst tensor A.
  Definition I_posttensor := posttensor I.
  Definition left_unitor := NaturalIsomorphism I_pretensor 1.
  Definition right_unitor := NaturalIsomorphism I_posttensor 1.

  Close Scope functor_scope.

  Variable alpha : associator.
  Variable lambda : left_unitor.
  Variable rho : right_unitor.
  Notation alpha_nat_trans := ((@morphism_isomorphic
                                  (C * (C * C) -> C)%category right_assoc left_assoc) alpha).
  Notation lambda_nat_trans := ((@morphism_isomorphic _ _ _) lambda).
  Notation rho_nat_trans := ((@morphism_isomorphic _ _ _) rho).

  Section coherence_laws.
    Variable a b c d : C.
  Local Definition P1 : (a ⊗ (b ⊗ (c ⊗ d))) --> (a ⊗ ((b ⊗ c) ⊗ d)).
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (b, tensor ₀ (c, d))))%object -->
(tensor ₀ (a, tensor ₀ (tensor ₀ (b, c), d)))%object
  Proof.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (b, tensor ₀ (c, d))))%object -->
(tensor ₀ (a, tensor ₀ (tensor ₀ (b, c), d)))%object
    apply (morphism_of tensor); split; simpl.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
a --> a
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (b, tensor ₀ (c, d)))%object -->
(tensor ₀ (tensor ₀ (b, c), d))%object
    -
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
a --> a exact (Core.identity a).
    -
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (b, tensor ₀ (c, d)))%object -->
(tensor ₀ (tensor ₀ (b, c), d))%object exact (alpha_nat_trans (b, (c, d))).
  Defined.

  Local Definition P2 : a ⊗ ((b ⊗ c) ⊗ d) --> (a ⊗ (b ⊗ c)) ⊗ d
    := alpha_nat_trans (a, (b ⊗ c, d)).
  Local Definition P3 : (a ⊗ (b ⊗ c)) ⊗ d --> ((a ⊗ b) ⊗ c ) ⊗ d.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (tensor ₀ (a, tensor ₀ (b, c)), d))%object -->
(tensor ₀ (tensor ₀ (tensor ₀ (a, b), c), d))%object
  Proof.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (tensor ₀ (a, tensor ₀ (b, c)), d))%object -->
(tensor ₀ (tensor ₀ (tensor ₀ (a, b), c), d))%object
    apply (morphism_of tensor); split; simpl.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (b, c)))%object -->
(tensor ₀ (tensor ₀ (a, b), c))%object
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
d --> d
    -
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (b, c)))%object -->
(tensor ₀ (tensor ₀ (a, b), c))%object exact (alpha_nat_trans (a,_)).
    -
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
d --> d exact (Core.identity d).
  Defined.
  Local Definition P4 : a ⊗ (b ⊗ (c ⊗ d)) --> (a ⊗ b) ⊗ (c ⊗ d)
    := alpha_nat_trans (a, (b, (c ⊗ d))).
  Local Definition P5 : (a ⊗ b) ⊗ (c ⊗ d) --> ((a ⊗ b) ⊗ c ) ⊗ d
    := alpha_nat_trans (a ⊗ b,(c, d)).

  Local Open Scope morphism_scope.
  Definition pentagon_eq := P3 o P2 o P1 = P5 o P4.
  Close Scope morphism_scope.

  Local Definition Q1 : (a ⊗ (I ⊗ b)) --> a ⊗ b.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (I, b)))%object -->
(tensor ₀ (a, b))%object
  Proof.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (I, b)))%object -->
(tensor ₀ (a, b))%object
    apply (morphism_of tensor); split; simpl.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
a --> a
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (I, b))%object --> b
    -
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
a --> a exact (Core.identity a).
    -
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (I, b))%object --> b exact (lambda_nat_trans _).
  Defined.

  Local Definition Q2 : (a ⊗ (I ⊗ b)) --> a ⊗ b.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (I, b)))%object -->
(tensor ₀ (a, b))%object
  Proof.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (I, b)))%object -->
(tensor ₀ (a, b))%object
    refine (@Category.Core.compose _ _ ((a ⊗ I) ⊗ b) _ _ _).
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (tensor ₀ (a, I), b))%object -->
(tensor ₀ (a, b))%object
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (I, b)))%object -->
(tensor ₀ (tensor ₀ (a, I), b))%object
    -
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (tensor ₀ (a, I), b))%object -->
(tensor ₀ (a, b))%object apply (morphism_of tensor); split; simpl.
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, I))%object --> a
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
b --> b
      +
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, I))%object --> a exact (rho_nat_trans a).
      +
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
b --> b exact (Core.identity b).
    -
H: Funext
C: PreCategory
tensor: (C * C -> C)%category
I: C
alpha: associator
lambda: left_unitor
rho: right_unitor
a, b, c, d: C
(tensor ₀ (a, tensor ₀ (I, b)))%object -->
(tensor ₀ (tensor ₀ (a, I), b))%object exact (alpha_nat_trans (a,(I,b))).
  Defined.
  Definition triangle_eq := Q1 = Q2.
  End coherence_laws.
End MonoidalCategoryConcepts.

Class MonoidalStructure (C : PreCategory) :=
  Build_MonoidalStructure {
    tensor : (C * C -> C)%category;
    I : C;
    alpha : associator tensor;
    lambda : left_unitor tensor I;
    rho : right_unitor tensor I;
    pentagon_eq_holds : forall a b c d : C, pentagon_eq alpha a b c d;
    triangle_eq_holds : forall a b : C, triangle_eq alpha lambda rho a b;
  }.

End MonoidalStructure.