open import Level
open import Level
open import Level
open import Category
module monoidal where

open import Data.Product renaming (_×_ to _*_)
open import Category.Constructions.Product
open import HomReasoning
open import cat-utility
open import Relation.Binary.Core
open import Relation.Binary

open Functor

record Iso  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
         (x y : Obj C )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
   field
         ≅→ :  Hom C x y 
         ≅← :  Hom C y x 
         iso→  :  C [ C [ ≅← o ≅→  ] ≈  id1 C x ]
         iso←  :  C [ C [ ≅→ o ≅←  ] ≈  id1 C y ]

record IsStrictMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  infixr 9 _□_
  _□_ : ( x y : Obj C ) → Obj C
  _□_ x y = FObj BI ( x , y )
  field
      mα : {a b c : Obj C} →  ( a □ b) □ c  ≡  a □ ( b □ c )
      mλ : (a : Obj C) → I □ a  ≡ a 
      mρ : (a : Obj C) → a □ I  ≡ a 

record StrictMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  field
      m-i : Obj C
      m-bi : Functor ( C × C ) C 
      isMonoidal : IsStrictMonoidal C m-i m-bi


--      non strict version includes 5 naturalities
record IsMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  open Iso 
  infixr 9 _□_ _■_
  _□_ : ( x y : Obj C ) → Obj C
  _□_ x y = FObj BI ( x , y )
  _■_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a □ b ) ( c □ d )
  _■_ f g = FMap BI ( f , g )
  field
      mα-iso : {a b c : Obj C} →  Iso C ( ( a □ b) □ c)  ( a □ ( b □ c ) ) 
      mλ-iso : {a : Obj C} →  Iso C ( I □ a)  a 
      mρ-iso : {a : Obj C} →  Iso C ( a □ I)  a 
      mα→nat1 : {a a' b c : Obj C} →  ( f : Hom C a a' ) →
         C [ C [ ( f ■ id1 C ( b □ c ))  o ≅→ (mα-iso {a} {b} {c}) ]  ≈
            C [   ≅→ (mα-iso )  o ( (f ■ id1 C b ) ■ id1 C c )    ] ]
      mα→nat2 : {a b b' c : Obj C} →  ( f : Hom C b b' ) →
         C [ C [ ( id1 C a ■ ( f ■ id1 C c ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
            C [   ≅→ (mα-iso )  o ( (id1 C a ■ f )  ■ id1 C c ) ] ]
      mα→nat3 : {a b c c' : Obj C} →  ( f : Hom C c c' ) →
         C [ C [ ( id1 C a ■ ( id1 C b ■ f ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
            C [   ≅→ (mα-iso )  o ( id1 C ( a □ b ) ■ f ) ] ]
      mλ→nat : {a a' : Obj C} →  ( f : Hom C a a' ) →
         C [ C [ f o ≅→ (mλ-iso {a} ) ]  ≈
            C [   ≅→ (mλ-iso )  o ( id1 C I  ■ f )    ] ]
      mρ→nat : {a a' : Obj C} →  ( f : Hom C a a' ) →
         C [ C [ f o ≅→ (mρ-iso {a} ) ]  ≈
            C [   ≅→ (mρ-iso )  o ( f ■ id1 C I  )    ] ]
  αABC□1D : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ (b □ c)) □ d)
  αABC□1D {a} {b} {c} {d} {e} = (  ≅→ mα-iso  ■ id1 C d )
  αAB□CD : {a b c d e : Obj C } → Hom C  ((a □ (b □ c)) □ d) (a □ ((b □ c ) □ d))
  αAB□CD {a} {b} {c} {d} {e} =   ≅→ mα-iso
  1A□BCD : {a b c d e : Obj C } → Hom C  (a □ ((b □ c ) □ d)) (a □ (b □ ( c □ d) ))
  1A□BCD {a} {b} {c} {d} {e} = ( id1 C a ■   ≅→ mα-iso )
  αABC□D : {a b c d e : Obj C } → Hom C  (a □ (b □ ( c □ d) )) ((a □ b ) □ (c □ d))
  αABC□D {a} {b} {c} {d} {e} =  ≅← mα-iso  
  αA□BCD : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ b ) □ (c □ d))
  αA□BCD {a} {b} {c} {d} {e} =  ≅→ mα-iso  
  αAIB :  {a b  : Obj C } →  Hom C (( a □ I ) □ b ) (a □ ( I □ b ))
  αAIB {a} {b} = ≅→ mα-iso
  1A□λB : {a b  : Obj C } →  Hom C  (a □ ( I □ b )) ( a □ b )
  1A□λB {a} {b} =  id1 C a ■  ≅→ mλ-iso 
  ρA□IB : {a b  : Obj C } →  Hom C  (( a □ I ) □ b ) ( a □ b )
  ρA□IB {a} {b} = ≅→  mρ-iso  ■  id1 C b

  field
      comm-penta : {a b c d e : Obj C}
         → C [ C [ αABC□D {a} {b} {c} {d} {e} o  C [ 1A□BCD {a} {b} {c} {d} {e} o C [ αAB□CD {a} {b} {c} {d} {e} o αABC□1D {a} {b} {c} {d} {e} ] ] ]
             ≈ αA□BCD {a} {b} {c} {d} {e} ]
      comm-unit : {a b : Obj C}
         → C [ C [ 1A□λB {a} {b} o  αAIB ] ≈ ρA□IB {a} {b} ]

record Monoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  field
      m-i : Obj C
      m-bi : Functor ( C × C ) C 
      isMonoidal : IsMonoidal C m-i m-bi


open import Category.Cat


record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
      ( MF :   Functor C D )
      ( F● :   Functor ( C × C ) D )
      ( F⊗ :   Functor ( C × C ) D )
      ( φab :  NTrans  ( C × C ) D  F● F⊗ )
      ( φ   :  Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) ) )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  _⊗_ : (x y : Obj C ) → Obj C
  _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
  _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d )
  _□_ f g = FMap (Monoidal.m-bi M) ( f , g )
  _●_ : (x y : Obj D ) → Obj D
  _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
  _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d )
  _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
  open Iso
  open Monoidal
  open IsMonoidal hiding ( _■_ ;  _□_ )
  αC :  {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
  αC {a} {b} {c} =  ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) 
  αD :  {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) )
  αD {a} {b} {c} =  ≅→ (mα-iso (isMonoidal N) {a} {b} {c}) 
  F : Obj C → Obj D
  F x = FObj MF x
  1●φBC :  {a b c : Obj C} → Hom D  ( F a ● ( F b ● F c ) ) ( F a ● ( F ( b ⊗ c ) ))
  1●φBC {a} {b} {c} =  id1 D (F a) ■  {!!}
  φAB⊗C :  {a b c : Obj C} → Hom D  ( F a ● ( F ( b ⊗ c ) )) (F ( a  ⊗ ( b  ⊗ c )))
  φAB⊗C {a} {b} {c} =  {!!}
  φAB●1 :  {a b c : Obj C} → Hom D  ( ( F a ●  F b ) ● F c ) ( F ( a ⊗ b ) ● F c )
  φAB●1 {a} {b} {c} =  {!!} ■ id1 D (F c)
  φA⊗BC :  {a b c : Obj C} → Hom D  ( F ( a ⊗ b ) ● F c ) (F ( (a  ⊗  b ) ⊗ c ))
  φA⊗BC {a} {b} {c} = {!!}
  FαC : {a b c : Obj C} → Hom D (F ( (a  ⊗  b ) ⊗ c )) (F ( a  ⊗ ( b  ⊗ c )))
  FαC {a} {b} {c} =  FMap MF ( ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) )
  1●φ : { a b : Obj C } → Hom D (F a  ● Monoidal.m-i N ) ( F a ● F ( Monoidal.m-i M ) )
  1●φ {a} {b} =  id1 D (F a)  ■  φ 
  φAIC : { a b : Obj C } → Hom D  ( F a ● F ( Monoidal.m-i M ) ) (F ( a  ⊗ Monoidal.m-i M ))
  φAIC {a} {b} = {!!}
  FρC : { a b : Obj C } → Hom D   (F ( a  ⊗ Monoidal.m-i M ))( F a  )
  FρC {a} {b} = FMap MF (  ≅→ (mρ-iso (isMonoidal M) {a} ) )
  ρD : { a b : Obj C } → Hom D (F a  ● Monoidal.m-i N ) ( F a  )
  ρD {a} {b} =  ≅→ (mρ-iso (isMonoidal N) {F a} )
  φ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b  ) ( F ( Monoidal.m-i M )  ● F b  )
  φ●1 {a} {b} =  φ  ■ id1 D (F b)
  φICB : { a b : Obj C } → Hom D  ( F ( Monoidal.m-i M )  ● F b  ) ( F (  ( Monoidal.m-i M )  ⊗ b ) )
  φICB {a} {b} = {!!}
  FλD : { a b : Obj C } → Hom D  ( F (  ( Monoidal.m-i M )  ⊗ b ) ) (F b ) 
  FλD {a} {b} = FMap MF ( ≅→ (mλ-iso (isMonoidal M) {b} ) )
  λD : { a b : Obj C } → Hom D  (Monoidal.m-i N ● F b  )  (F b ) 
  λD {a} {b} = ≅→ (mλ-iso (isMonoidal N) {F b} )
  field
     comm1 : {a b c : Obj C } → D [ D [ φAB⊗C {a} {b} {c} o D [ 1●φBC o αD ] ]  ≈ D [ FαC  o  D [ φA⊗BC o φAB●1 ] ] ]
     comm-idr : {a b : Obj C } → D [ D [ FρC  {a} {b}  o D [ φAIC {a} {b} o  1●φ {a} {b} ] ]  ≈ ρD {a} {b}  ]
     comm-idl : {a b : Obj C } → D [ D [ FλD  {a} {b}  o D [ φICB {a} {b} o  φ●1 {a} {b} ] ]  ≈ λD {a} {b}  ]

record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  _⊗_ : (x y : Obj C ) → Obj C
  _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
  _●_ : (x y : Obj D ) → Obj D
  _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
  field
      MF : Functor C D
  F● :  Functor ( C × C ) D
  F●  =  record {
       FObj = λ x  → (FObj MF (proj₁ x) ) ●  (FObj MF (proj₂ x) )
     ; FMap = λ {x : Obj ( C × C ) } {y} f → FMap (Monoidal.m-bi N) (  FMap MF  (proj₁  f ) , FMap MF (proj₂ f)  )
     ; isFunctor = record {
     }
    }
  F⊗ : Functor ( C × C ) D
  F⊗  =  record {
       FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x )
     ; FMap = λ {a} {b} f →  FMap MF ( FMap (Monoidal.m-bi M) (  proj₁ f , proj₂ f) )
     ; isFunctor = record {
     }
    }
  field
      φab :  NTrans  ( C × C ) D  F● F⊗ 
      φ   : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
      isMonodailFunctor : IsMonoidalFunctor  M N MF F● F⊗ φab φ