{-# OPTIONS --lossy-unification #-}
module Cubical.Categories.Presheaf.Constructions.BinProduct.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure

import Cubical.Data.Equality as Eq
open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Profunctor.General
open import Cubical.Categories.FunctorComprehension
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Constructions.BinProduct
open import Cubical.Categories.Constructions.BinProduct.More
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.Sets.More
open import Cubical.Categories.Presheaf.Base
open import Cubical.Categories.Presheaf.Constructions.Reindex
open import Cubical.Categories.Presheaf.Constructions.Tensor
open import Cubical.Categories.Presheaf.More
open import Cubical.Categories.Presheaf.Morphism.Alt
open import Cubical.Categories.Profunctor.Constructions.Extension
open import Cubical.Categories.Bifunctor
open import Cubical.Categories.Yoneda.More

private
  variable
    ℓ ℓ' ℓA ℓB ℓA' ℓB' ℓC ℓC' ℓD ℓD' ℓP ℓQ ℓR ℓS : Level

open Functor
open PshHom
open PshIso

module _ {C : Category ℓ ℓ'} where
  private
    module C = Category C
  PshProd' : Functor
    (PresheafCategory C ℓA ×C PresheafCategory C ℓB)
    (PresheafCategory C (ℓ-max ℓA ℓB))
  PshProd' = (postcomposeF _ ×Sets ∘F ,F-functor)

  PshProd : Bifunctor (PresheafCategory C ℓA) (PresheafCategory C ℓB)
                      (PresheafCategory C (ℓ-max ℓA ℓB))
  PshProd = ParFunctorToBifunctor PshProd'

  -×Psh_ : Presheaf C ℓA → Functor (PresheafCategory C ℓB) (PresheafCategory C (ℓ-max ℓA ℓB))
  -×Psh Q = appR PshProd Q

  _×Psh- : Presheaf C ℓA → Functor (PresheafCategory C ℓB) (PresheafCategory C (ℓ-max ℓA ℓB))
  P ×Psh- = appL PshProd P

  _×Psh_ : Presheaf C ℓA → Presheaf C ℓB → Presheaf C _
  P ×Psh Q = PshProd ⟅ P , Q ⟆b

  -- irritatingly not definitional...
  -×Psh-Fob : ∀ (P : Presheaf C ℓP) (Q : Presheaf C ℓQ)
    → PshIso (P ×Psh Q) ((-×Psh Q) ⟅ P ⟆)
  -×Psh-Fob P Q = eqToPshIso (F-ob (-×Psh Q) P) Eq.refl Eq.refl

  private
    testPshProd : ∀ (P : Presheaf C ℓA)(Q : Presheaf C ℓB)
      → P ×Psh Q ≡ ×Sets ∘F (P ,F Q)
    testPshProd P Q = refl

  module _ (P : Presheaf C ℓA)(Q : Presheaf C ℓB) where
    π₁ : PshHom (P ×Psh Q) P
    π₁ .N-ob _ = fst
    π₁ .N-hom _ _ _ _ = refl

    π₂ : PshHom (P ×Psh Q) Q
    π₂ .N-ob _ = snd
    π₂ .N-hom _ _ _ _ = refl

  module _
    {P : Presheaf C ℓA}
    {Q : Presheaf C ℓB}
    {R : Presheaf C ℓA'}
    (α : PshHom R P)
    (β : PshHom R Q)
    where
    ×PshIntro : PshHom R (P ×Psh Q)
    ×PshIntro .N-ob c x = (α .N-ob c x) , (β .N-ob c x)
    ×PshIntro .N-hom c c' f p =
      cong₂ _,_ (α .N-hom c c' f p) (β .N-hom c c' f p)

    ×Pshβ₁ : ×PshIntro ⋆PshHom π₁ P Q ≡ α
    ×Pshβ₁ = makePshHomPath refl

    ×Pshβ₂ : ×PshIntro ⋆PshHom π₂ P Q ≡ β
    ×Pshβ₂ = makePshHomPath refl

  ΔPshHom : {P : Presheaf C ℓA} → PshHom P (P ×Psh P)
  ΔPshHom = ×PshIntro idPshHom idPshHom

  module _ (P : Presheaf C ℓA)(Q : Presheaf C ℓB) where
    ×Psh-UMP : ∀ {R : Presheaf C ℓA'} → Iso (PshHom R (P ×Psh Q)) (PshHom R P × PshHom R Q)
    ×Psh-UMP .Iso.fun α = (α ⋆PshHom π₁ P Q) , (α ⋆PshHom π₂ P Q)
    ×Psh-UMP .Iso.inv (α , β) = ×PshIntro α β
    ×Psh-UMP .Iso.rightInv (α , β) = ΣPathP ((×Pshβ₁ α β) , (×Pshβ₂ α β))
    ×Psh-UMP .Iso.leftInv α = makePshHomPath refl

  module _
    {P : Presheaf C ℓA}
    {P' : Presheaf C ℓA'}
    {Q : Presheaf C ℓB}
    {Q' : Presheaf C ℓB'}
    where
    _×PshHom_ : PshHom P P' → PshHom Q Q' → PshHom (P ×Psh Q) (P' ×Psh Q')
    α ×PshHom β = ×PshIntro (π₁ P Q ⋆PshHom α) (π₂ P Q ⋆PshHom β)
  module _
    {P : Presheaf C ℓA}
    {P' : Presheaf C ℓA'}
    {Q : Presheaf C ℓB}
    {Q' : Presheaf C ℓB'}
    (PIso : PshIso P P')
    (QIso : PshIso Q Q')
    where
    ×PshIso : PshIso (P ×Psh Q) (P' ×Psh Q')
    ×PshIso .trans = (PIso .trans ×PshHom QIso .trans)
    ×PshIso .nIso c .fst x =
      PIso .nIso c .fst (x .fst) ,
      QIso .nIso c .fst (x .snd)
    ×PshIso .nIso c .snd .fst b =
      cong₂ _,_
        (PIso .nIso c .snd .fst (b .fst))
        (QIso .nIso c .snd .fst (b .snd))
    ×PshIso .nIso c .snd .snd b =
      cong₂ _,_
        (PIso .nIso c .snd .snd (b .fst))
        (QIso .nIso c .snd .snd (b .snd))

  private
    open Category
    open Bifunctor
    open NatTrans
    -- Test to make sure we get the right definitional
    -- behavior for Bif-homL, Bif-homR
    module _ (P P' : Presheaf C ℓA)(Q Q' : Presheaf C ℓB)
             (α : PresheafCategory C ℓA [ P , P' ])
             (β : PresheafCategory C ℓB [ Q , Q' ])
             c where

      _ : PshProd .Bif-homL α Q .N-ob c ≡ λ (p , q) → α .N-ob c p , q
      _ = refl

      _ : PshProd .Bif-homR P β .N-ob c ≡ λ (p , q) → p , β .N-ob c q
      _ = refl

module _ {C : Category ℓ ℓ'}{D : Category ℓD ℓD'}
  (F : Functor D C)
  (P : Presheaf C ℓA)(Q : Presheaf C ℓB) where
  reindPsh× : PshIso (reindPsh F (P ×Psh Q)) (reindPsh F P ×Psh reindPsh F Q)
  reindPsh× .trans = ×PshIntro (reindPshHom F (π₁ P Q)) (reindPshHom F (π₂ P Q))
  reindPsh× .nIso x .fst = λ z → z
  reindPsh× .nIso x .snd .fst b = refl
  reindPsh× .nIso x .snd .snd a = refl

module _ {C : Category ℓ ℓ'}{D : Category ℓD ℓD'} where
  -- (R(d,c) ⊗[ c ] Q(c,*)) × P(d,*) ≅ (R(d,c) × P(d,*)) ⊗[ c ] Q(c,*)
  ⊗×-comm : (R : Bifunctor (D ^op) C (SET ℓR)) (P : Presheaf D ℓP) (Q : Presheaf C ℓQ)
    → PshIso ((ext R ⟅ Q ⟆) ×Psh P) (ext (CurriedToBifunctorL ((-×Psh P) ∘F CurryBifunctorL R)) ⟅ Q ⟆)
  ⊗×-comm R P Q = pshiso (pshhom
    (λ d → uncurry (R⊗Q.rec (isSet→ extR×PQ.isSetPsh)
      (λ r q p → (r , p) R×P⊗Q.,⊗ q) (λ r f q → funExt λ p → R×P⊗Q.swap (r , p) f q)))
    λ c c' f → uncurry (R⊗Q.ind (λ _ → isPropΠ (λ _ → extR×PQ.isSetPsh _ _))
      (λ r q p → refl)))
    λ d → (R×P⊗Q.rec extRQ×P.isSetPsh (λ (r , p) q → (r R⊗Q.,⊗ q) , p) λ (r , p) f q → ΣPathP ((R⊗Q.swap r f q) , refl))
    , R×P⊗Q.ind (λ _ → extR×PQ.isSetPsh _ _) (λ _ _ → refl)
    , uncurry (R⊗Q.ind (λ _ → isPropΠ (λ _ → extRQ×P.isSetPsh _ _)) λ _ _ _ → refl)
    where
      module extRQ = PresheafNotation (ext R ⟅ Q ⟆)
      module extRQ×P = PresheafNotation ((ext R ⟅ Q ⟆) ×Psh P)
      module R⊗Q = ext-⊗ R Q
      module R×P⊗Q = ext-⊗ (CurriedToBifunctorL ((-×Psh P) ∘F CurryBifunctorL R)) Q
      module extR×PQ = PresheafNotation (ext (CurriedToBifunctorL ((-×Psh P) ∘F CurryBifunctorL R)) ⟅ Q ⟆)
      module P = PresheafNotation P

module _ {C : Category ℓ ℓ'} where
  private
    module C = Category C

  -×Psh_-cocontinuous : (P : Presheaf C ℓA) → CoContinuous (-×Psh P)
  -×Psh P -cocontinuous Q =
    invPshIso (-×Psh-Fob Q P) -- just expanding definitions
  -- Q(c,*) × P(c,*)
    ⋆PshIso ((×PshIso (CoYoneda Q) idPshIso)
  -- (C(c,c') ⊗[ c' ] Q(c',*)) × P(c,*)
    ⋆PshIso (⊗×-comm (HomBif C) P Q))
  -- (C(c,c') × P(c,*)) ⊗[ c' ] Q(c',*)