Require Import Basics.Utf8.Require Import Basics.Utf8.
Require Import Category.Core Category.Morphisms.
Require Import Functor.Core
        Functor.Utf8.
Require Import NaturalTransformation.Core.
Require Import FunctorCategory.Core FunctorCategory.Morphisms.
Require Import ProductLaws.

Set Implicit Arguments.
Generalizable All Variables.

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.