{-

  If M and N are monoidal categories, then weaken M.C N.C can be given
  the structure of a displayed monoidal category.

-}
module Cubical.Categories.Displayed.Instances.TotalCategory.Monoidal where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Monoidal.Base
open import Cubical.Categories.Instances.BinProduct.Monoidal

open import Cubical.Categories.Displayed.Base
open import Cubical.Categories.Displayed.Functor
open import Cubical.Categories.Displayed.NaturalTransformation
open import Cubical.Categories.Displayed.NaturalTransformation.More
open import Cubical.Categories.Displayed.Monoidal.Base
open import Cubical.Categories.Displayed.Limits.Terminal
open import Cubical.Categories.Displayed.Limits.BinProduct
import Cubical.Categories.Displayed.Reasoning as Reasoning
import Cubical.Categories.Displayed.Instances.Weaken.Base as Wk
import Cubical.Categories.Displayed.Instances.SimpleTotalCategoryR
  as TotalCatᴰ

private
  variable
    ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level

module _ (M : MonoidalCategory ℓC ℓC')
         (N : MonoidalCategory ℓD ℓD')
         (P : MonoidalCategoryᴰ (M ×M N) ℓE ℓE')
         where
  open Category
  open MonoidalCategoryᴰ
  open TensorStrᴰ
  open MonoidalStrᴰ
  open Functorᴰ
  open Functor
  open NatTransᴰ
  open NatIsoᴰ
  open isIsoᴰ
  open NatTrans
  open NatIso
  open isIso
  private
    module M = MonoidalCategory M
    module N = MonoidalCategory N
    module P = MonoidalCategoryᴰ P
    module PR = Reasoning P.Cᴰ

  ∫Mᴰsr : MonoidalCategoryᴰ M (ℓ-max ℓD ℓE) (ℓ-max ℓD' ℓE')
  ∫Mᴰsr .Cᴰ = TotalCatᴰ.∫Cᴰsr {C = M.C}{D = N.C} P.Cᴰ
  -- TODO: maybe could have used an intro principle for ∫Cᴰsr here
  -- TODO: maybe all of this could be from intro principles for ∫Cᴰ?
  ∫Mᴰsr .monstrᴰ .tenstrᴰ .─⊗ᴰ─ .F-obᴰ {m , m'}
    ((n , p) , (n' , p')) = (n N.⊗ n') , (p P.⊗ᴰ p')
  ∫Mᴰsr .monstrᴰ .tenstrᴰ .─⊗ᴰ─ .F-homᴰ
    ((f , fᴰ) , (g , gᴰ)) = (f N.⊗ₕ g) , (fᴰ P.⊗ₕᴰ gᴰ)
  ∫Mᴰsr .monstrᴰ .tenstrᴰ .─⊗ᴰ─ .F-idᴰ =
    ΣPathP ((N.─⊗─ .F-id) , PR.rectify (P.─⊗ᴰ─ .F-idᴰ))
  ∫Mᴰsr .monstrᴰ .tenstrᴰ .─⊗ᴰ─ .F-seqᴰ fᴰ gᴰ =
    ΣPathP ((N.─⊗─ .F-seq _ _) , PR.rectify (P.─⊗ᴰ─ .F-seqᴰ _ _))
  ∫Mᴰsr .monstrᴰ .tenstrᴰ .unitᴰ = N.unit , P.unitᴰ
  ∫Mᴰsr .monstrᴰ .αᴰ .transᴰ .N-obᴰ xᴰ =
    N.α⟨ _ , _ , _ ⟩ , P.αᴰ⟨ _ , _ , _ ⟩
  ∫Mᴰsr .monstrᴰ .αᴰ .transᴰ .N-homᴰ fᴰ = ΣPathP
    (N.α .trans .N-hom _ , P.αᴰ .transᴰ .N-homᴰ _)
  ∫Mᴰsr .monstrᴰ .αᴰ .nIsoᴰ xᴰ .invᴰ =
    N.α⁻¹⟨ _ , _ , _ ⟩ , P.α⁻¹ᴰ⟨ _ , _ , _ ⟩
  ∫Mᴰsr .monstrᴰ .αᴰ .nIsoᴰ xᴰ .secᴰ =
    ΣPathP ((N.α .nIso _ .sec) , (P.αᴰ .nIsoᴰ _ .secᴰ))
  ∫Mᴰsr .monstrᴰ .αᴰ .nIsoᴰ xᴰ .retᴰ =
    ΣPathP ((N.α .nIso _ .ret) , (P.αᴰ .nIsoᴰ _ .retᴰ))
  ∫Mᴰsr .monstrᴰ .ηᴰ .transᴰ .N-obᴰ _ = N.η⟨ _ ⟩ , P.ηᴰ⟨ _ ⟩
  ∫Mᴰsr .monstrᴰ .ηᴰ .transᴰ .N-homᴰ _ =
    ΣPathP (N.η .trans .N-hom _ , P.ηᴰ .transᴰ .N-homᴰ _)
  ∫Mᴰsr .monstrᴰ .ηᴰ .nIsoᴰ xᴰ .invᴰ = N.η⁻¹⟨ _ ⟩ , P.η⁻¹ᴰ⟨ _ ⟩
  ∫Mᴰsr .monstrᴰ .ηᴰ .nIsoᴰ xᴰ .secᴰ =
    ΣPathP ((N.η .nIso _ .sec) , (P.ηᴰ .nIsoᴰ _ .secᴰ))
  ∫Mᴰsr .monstrᴰ .ηᴰ .nIsoᴰ xᴰ .retᴰ =
    ΣPathP ((N.η .nIso _ .ret) , (P.ηᴰ .nIsoᴰ _ .retᴰ))
  ∫Mᴰsr .monstrᴰ .ρᴰ .transᴰ .N-obᴰ _ = N.ρ⟨ _ ⟩ , P.ρᴰ⟨ _ ⟩
  ∫Mᴰsr .monstrᴰ .ρᴰ .transᴰ .N-homᴰ _ =
    ΣPathP (N.ρ .trans .N-hom _ , P.ρᴰ .transᴰ .N-homᴰ _)
  ∫Mᴰsr .monstrᴰ .ρᴰ .nIsoᴰ xᴰ .invᴰ = N.ρ⁻¹⟨ _ ⟩ , P.ρ⁻¹ᴰ⟨ _ ⟩
  ∫Mᴰsr .monstrᴰ .ρᴰ .nIsoᴰ xᴰ .secᴰ =
    ΣPathP ((N.ρ .nIso _ .sec) , (P.ρᴰ .nIsoᴰ _ .secᴰ))
  ∫Mᴰsr .monstrᴰ .ρᴰ .nIsoᴰ xᴰ .retᴰ =
    ΣPathP ((N.ρ .nIso _ .ret) , (P.ρᴰ .nIsoᴰ _ .retᴰ))
  ∫Mᴰsr .monstrᴰ .pentagonᴰ wᴰ xᴰ yᴰ zᴰ =
    ΣPathP (N.pentagon _ _ _ _ , P.pentagonᴰ _ _ _ _)
  ∫Mᴰsr .monstrᴰ .triangleᴰ _ _ = ΣPathP (N.triangle _ _ , P.triangleᴰ _ _)