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 _≅_ {ℓ : Level } ( C B : Set ℓ ) : Set  (suc ℓ )  where
   field
         ≅→ : C → B
         ≅← : B → C
         ≅Id→  :  {x : C} →  ≅← ( ≅→ x  ) ≡  x
         ≅Id←  :  {x : B} →  ≅→ ( ≅← x  ) ≡  x

infix  4 _≅_

record IsMonoidal  {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 : (a : Obj C) → I ⊗ a  ≡ a 
      mσa : (a : Obj C) → a ⊗ I  ≡ a 

--      -- non strict version includes 6 naturalities
--      mα→ : {a b c : Obj C} → Hom C ( ( a ⊗ b) ⊗ c)  ( a ⊗ ( b ⊗ c ) )
--      mα← : {a b c : Obj C} → Hom C ( a ⊗ ( b ⊗ c )) ( ( a ⊗ b) ⊗ c)
--      mα-iso→ : {a b c : Obj C} →  C [ C [ mα←  o  mα→ ] ≈ id1 C (( a ⊗  b)  ⊗ c )  ] 
--      mα-iso← : {a b c : Obj C} →  C [ C [ mα→  o  mα← ] ≈ id1 C (  a ⊗ (b   ⊗ c )) ] 
--      mα→nat1 : {a a' b c : Obj C} →  ( f : Hom C a a' ) →
--         C [ C [ FMap BI ( f , id1 C (FObj BI ( b , c )  ))  o mα→ {a} ]  ≈
--            C [   mα→ {a'}  o FMap BI ( FMap BI (f , id1 C b ) , id1 C c )    ] ]

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 )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  field
     a : {!!}

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