{-# OPTIONS --type-in-type #-}

module Monoidal where

open import Base

-- ℂ
record IsParamMonoidalCategory
       {c : Set} {MonoidalProduct₀ : c × c → c} {Identity₀ : ⊤ → c}
       (ℂ : ParamCategory c)
       (MonoidalProduct : ParamFunctor (ParamProduct ℂ ℂ) ℂ MonoidalProduct₀)
       (funcI : ParamFunctor 𝟙 ℂ Identity₀) : Set where
  open ParamCategory ℂ
  module MonoidalProduct = ParamFunctor MonoidalProduct
  module funcI = ParamFunctor funcI

  infixr  _⊗_
  infixr  _⊗₁_

  _⊗_ : c → c → c
  _⊗_ = λ x y → MonoidalProduct₀ (x , y)
  _⊗₁_ : ∀ {X Y U V} → hom X Y → hom U V → hom (X ⊗ U) (Y ⊗ V)
  _⊗₁_ = λ x y → MonoidalProduct.F₁ (x , y)
  I = Identity₀ tt
  I₁ = funcI.F₁ tt
  field
    λ-at : ∀ X → hom (I ⊗ X) X
    λ-naturality : ∀ {A B} (f : hom A B) → I₁ ⊗₁ f ▷ λ-at B ≡ λ-at A ▷ f
    ρ-at : ∀ X → hom X (X ⊗ I)
    ρ-naturality : ∀ {A B} (f : hom A B) → ρ-at A ▷ f ⊗₁ I₁ ≡ f ▷ ρ-at B
    α-at : ∀ X Y Z → hom ((X ⊗ Y) ⊗ Z) (X ⊗ (Y ⊗ Z))
    α-naturality : ∀ {A B C D E F} (f : hom A B) (g : hom C D) (h : hom E F)
                   → (f ⊗₁ g) ⊗₁ h ▷ α-at B D F ≡ α-at A C E ▷ f ⊗₁ (g ⊗₁ h) 
    triangle : ∀ X Y → α-at X I Y ▷ id X ⊗₁ λ-at Y ▷ ρ-at X ⊗₁ (id Y)
                       ≡ id ((X ⊗ I) ⊗ Y)
    pentagon : ∀ X Y Z W → α-at X Y Z ⊗₁ id W
                         ▷ α-at X (Y ⊗ Z) W
                         ▷ id X ⊗₁ α-at Y Z W
                         ≡ α-at (X ⊗ Y) Z W ▷ α-at X Y (Z ⊗ W)


-- if it ends in Category, it exposes all the category stuff on the same level
record ParamMonoidalCategory
       (c : Set) (⊗₀ : c × c → c) (I₀ : ⊤ → c) : Set where
  field
    P : ParamCategory c
  U = record { obj = c ; PC = P }
  open ParamCategory P
  field
    MonoidalProduct : ParamFunctor (ParamProduct P P) P ⊗₀
    funcI : ParamFunctor 𝟙 P I₀
    isParamMonoidalCategory : IsParamMonoidalCategory P MonoidalProduct funcI
  open ParamCategory P public
  open IsParamMonoidalCategory isParamMonoidalCategory public
  obj = c


record MonoidalCategory : Set where
  field
    c : Set
    MonoidalProduct₀ : c × c → c
    Identity₀ : ⊤ → c
    P-monoidal : ParamMonoidalCategory c MonoidalProduct₀ Identity₀
  open ParamMonoidalCategory P-monoidal public

-- 𝕂
record IsParamMonoidalLikeCategory
       {c : Set} {MonoidalLikeProduct₀ : c × c → c} {Identity₀ : ⊤ → c}
       (ℂ : ParamCategory c)
       (MonoidalLikeProduct : ParamLaxFunctor (ParamProduct ℂ ℂ) ℂ MonoidalLikeProduct₀)
       (LikeI : ParamLaxFunctor 𝟙 ℂ Identity₀) : Set where
  open ParamCategory ℂ
  module MonoidalLikeProduct = ParamLaxFunctor MonoidalLikeProduct
  module LikeI = ParamLaxFunctor LikeI

  infixr  _⊗_
  infixr  _∥_

  _⊗_ : c → c → c
  _⊗_ = λ x y → MonoidalLikeProduct₀ (x , y)
  _∥_ : ∀ {X Y U V} → hom X Y → hom U V → hom (X ⊗ U) (Y ⊗ V)
  _∥_ = λ x y → MonoidalLikeProduct.F₁ (x , y)
  I = Identity₀ tt
  jd = LikeI.F₁ tt
  field
    λ-at : ∀ X → hom (I ⊗ X) X
    λ-naturality : ∀ {A B} {f : hom A B} → jd ∥ f ▷ λ-at B ≡ λ-at A ▷ f
    ρ-at : ∀ X → hom X (X ⊗ I)
    ρ-naturality : ∀ {A B} {f : hom A B} → ρ-at A ▷ f ∥ jd ≡ f ▷ ρ-at B
    α-at : ∀ X Y Z → hom ((X ⊗ Y) ⊗ Z) (X ⊗ (Y ⊗ Z))
    α-naturality : ∀ {A B C D E F} {f : hom A B} {g : hom C D} {h : hom E F}
      → ((f ∥ g) ∥ h) ▷ α-at B D F ≡ α-at A C E ▷ (f ∥ (g ∥ h)) 
    triangle : ∀ X Y → (α-at X I Y) ▷ (id X) ∥ λ-at Y ▷ ρ-at X ∥ (id Y) ≡
             id  ((X ⊗ I) ⊗ Y)
    pentagon : ∀ X Y Z W → (α-at X Y Z) ∥ (id W)
                               ▷ (α-at X (Y ⊗ Z) W)
                               ▷ (id X) ∥ (α-at Y Z W)
                          ≡ (α-at (X ⊗ Y) Z W) ▷ (α-at X Y (Z ⊗ W))
    

record ParamMonoidalLikeCategory
       (c : Set) (⊗₀ : c × c → c) (I₀ : ⊤ → c) : Set where
  field
    P : ParamCategory c
  U = record { obj = c ; PC = P }  
  open ParamCategory P
  field
    MonoidalLikeProduct : ParamLaxFunctor (ParamProduct P P) P ⊗₀
    funcLikeI : ParamLaxFunctor 𝟙 P I₀
    isParamMonoidalLikeCategory : IsParamMonoidalLikeCategory P MonoidalLikeProduct funcLikeI
  open ParamCategory P public
  open IsParamMonoidalLikeCategory isParamMonoidalLikeCategory public
  obj = c
  
record MonoidalLikeCategory : Set where
  field
    c : Set
    t⊗₀ : c × c → c
    tI₀ : ⊤ → c
    P-monoidallike : ParamMonoidalLikeCategory c t⊗₀ tI₀
  open ParamMonoidalLikeCategory P-monoidallike public