indexsource

open import Cat.Prelude
open import Cat.Functor.Base
open import Cat.Functor.Compose
open import Cat.Functor.Equivalence.Path
open import Cat.Monoidal.Base
open import Cat.Monoidal.Diagram.Monoid
open import Cat.Instances.Product
open import Cat.Displayed.Base
open import Cat.Displayed.Total

open Monoidal-category
open Precategory
open Functor
open _=>_

-- ⚠️ WIP ⚠️
module PointwiseMonoidal
  {o o′  ℓ′} (C : Precategory o ) (D : Precategory o′ ℓ′)
  (M : Monoidal-category D)
  where

Pointwise : Monoidal-category Cat[ C , D ]
Pointwise = pw where
  prod : Functor (Cat[ C , D ] ×ᶜ Cat[ C , D ]) Cat[ C , D ]
  prod .F₀ (a , b) = M .-⊗- F∘ Cat⟨ a , b 
  prod .F₁ {x = x} {y = y} (na , nb) = M .-⊗-  nat where
    nat : Cat⟨ x .fst , x .snd  => Cat⟨ y .fst , y .snd 
    nat .η x = (na .η x) , (nb .η x)
    nat .is-natural x y f i = (na .is-natural x y f i) , (nb .is-natural x y f i)
  prod .F-id = ext λ _  M .-⊗- .F-id
  prod .F-∘ f g = ext λ _  M .-⊗- .F-∘ _ _
  pw : Monoidal-category Cat[ C , D ]
  pw .-⊗- = prod
  pw .Unit = Const (M .Unit)
  pw .unitor-l = {! M .unitor-l  !}
  pw .unitor-r = {!   !}
  pw .associator = {!   !}
  pw .triangle = {!   !}
  pw .pentagon = {!   !}

MonCD→CMonD : Functor ( Mon[ Pointwise ]) (Cat[ C ,  Mon[ M ] ])
MonCD→CMonD .F₀ (F , mon) .F₀ c = F .F₀ c , {!   !}
MonCD→CMonD .F₀ (F , mon) .F₁ = {!   !}
MonCD→CMonD .F₀ (F , mon) .F-id = {!   !}
MonCD→CMonD .F₀ (F , mon) .F-∘ = {!   !}
MonCD→CMonD .F₁ = {!   !}
MonCD→CMonD .F-id = {!   !}
MonCD→CMonD .F-∘ = {!   !}

MonCD≡CMonD :  Mon[ Pointwise ]  Cat[ C ,  Mon[ M ] ]
MonCD≡CMonD = Precategory-path MonCD→CMonD {!   !}