{-# OPTIONS --lossy-unification #-}
module Cubical.Categories.Displayed.Instances.Presheaf.General where

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

open import Cubical.Data.Sigma

open import Cubical.Categories.Category
open import Cubical.Categories.Constructions.Fiber
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Presheaf.Base
open import Cubical.Categories.Presheaf.Morphism.Alt
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Presheaf.Representable.More

open import Cubical.Categories.Displayed.Base
open import Cubical.Categories.Displayed.Exponentials.Small
open import Cubical.Categories.Displayed.Fibration.Base
open import Cubical.Categories.Displayed.Instances.Functor
open import Cubical.Categories.Displayed.Instances.Sets.Base
open import Cubical.Categories.Displayed.Limits.CartesianV
open import Cubical.Categories.Displayed.Limits.BinProduct
open import Cubical.Categories.Displayed.Limits.Terminal
open import Cubical.Categories.Displayed.Presheaf
open import Cubical.Categories.Displayed.Presheaf.Constructions.Reindex
open import Cubical.Categories.Displayed.Presheaf.Constructions.Lift
open import Cubical.Categories.Displayed.Presheaf.Constructions.Unit
open import Cubical.Categories.Displayed.Presheaf.Constructions.BinProduct
open import Cubical.Categories.Displayed.Presheaf.Constructions.Exponential

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

open Category
open Categoryᴰ
-- TODO: move these upstream
PRESHEAF : (C : Category ℓC ℓC') (ℓP : Level) → Category _ _
PRESHEAF C ℓP .ob = Presheaf C ℓP
PRESHEAF C ℓP .Hom[_,_] = PshHom
PRESHEAF C ℓP .id = idPshHom
PRESHEAF C ℓP ._⋆_ = _⋆PshHom_
PRESHEAF C ℓP .⋆IdL = λ f → makePshHomPath refl
PRESHEAF C ℓP .⋆IdR = λ f → makePshHomPath refl
PRESHEAF C ℓP .⋆Assoc = ⋆PshHomAssoc
PRESHEAF C ℓP .isSetHom = isSetPshHom _ _

-- TODO: move upstream
PRESHEAFᴰ' : {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ')
  → ∀ (ℓP ℓPᴰ : Level) → Categoryᴰ (PRESHEAF C ℓP) _ _
PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ .ob[_] P = Presheafᴰ P Cᴰ ℓPᴰ
PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ .Hom[_][_,_] α Pᴰ Qᴰ = PshHomᴰ α Pᴰ Qᴰ
PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ .idᴰ = idPshHomᴰ
PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ ._⋆ᴰ_ = _⋆PshHomᴰ_
PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ .⋆IdLᴰ {P}{Q}{α}{Pᴰ}{Qᴰ} αᴰ = makePshHomᴰPathP _ _ _ (funExt (λ p → Qᴰ.rectify (Qᴰ.≡out refl)))
  where module Qᴰ = PresheafᴰNotation Qᴰ
PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ .⋆IdRᴰ {P}{Q}{α}{Pᴰ}{Qᴰ} αᴰ = makePshHomᴰPathP _ _ _ (funExt (λ p → Qᴰ.rectify (Qᴰ.≡out refl)))
  where module Qᴰ = PresheafᴰNotation Qᴰ
PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ .⋆Assocᴰ {wᴰ = Sᴰ} αᴰ βᴰ γᴰ = makePshHomᴰPathP _ _ _ (funExt (λ p → Sᴰ.rectify (Sᴰ.≡out refl)))
  where module Sᴰ = PresheafᴰNotation Sᴰ
PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ .isSetHomᴰ = isSetPshHomᴰ _ _ _

module _ {ℓP ℓQ ℓPᴰ ℓQᴰ ℓRᴰ ℓSᴰ}{C : Category ℓC ℓC'}{Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
  {P : Presheaf C ℓP}{Q : Presheaf C ℓQ}
  {Pᴰ : Presheafᴰ P Cᴰ ℓPᴰ}{Qᴰ : Presheafᴰ Q Cᴰ ℓQᴰ}{Rᴰ : Presheafᴰ Q Cᴰ ℓRᴰ}{Sᴰ : Presheafᴰ Q Cᴰ ℓSᴰ}
  {α : PshHom P Q} where
  ⋆PshHomAssocᴰⱽⱽ : (αᴰ : PshHomᴰ α Pᴰ Qᴰ)(βᴰ : PshHomⱽ Qᴰ Rᴰ)(γᴰ : PshHomⱽ Rᴰ Sᴰ)
    → (αᴰ ⋆PshHomᴰⱽ βᴰ) ⋆PshHomᴰⱽ γᴰ ≡ αᴰ ⋆PshHomᴰⱽ (βᴰ ⋆PshHomⱽ γᴰ)
  ⋆PshHomAssocᴰⱽⱽ αᴰ βᴰ γᴰ = makePshHomᴰPath refl

module _ {ℓP ℓQ ℓPᴰ ℓQᴰ}{C : Category ℓC ℓC'}{Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
  {P : Presheaf C ℓP}{Q : Presheaf C ℓQ}
  {α : PshHom P Q}
  {Pᴰ : Presheafᴰ P Cᴰ ℓPᴰ}{Qᴰ : Presheafᴰ Q Cᴰ ℓQᴰ}
  where
  ⋆PshHomIdRᴰⱽ : (αᴰ : PshHomᴰ α Pᴰ Qᴰ) → αᴰ ⋆PshHomᴰⱽ idPshHomᴰ ≡ αᴰ
  ⋆PshHomIdRᴰⱽ αᴰ = makePshHomᴰPath refl

module _ {ℓP ℓQ ℓPᴰ ℓQᴰ ℓRᴰ}{C : Category ℓC ℓC'}{Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
  {P : Presheaf C ℓP}{Q : Presheaf C ℓQ}
  {Pᴰ : Presheafᴰ P Cᴰ ℓPᴰ}{Qᴰ : Presheafᴰ Q Cᴰ ℓQᴰ}{Rᴰ : Presheafᴰ Q Cᴰ ℓRᴰ}
  where
  private
    module Pᴰ = PresheafᴰNotation Pᴰ
    module Rᴰ = PresheafᴰNotation Rᴰ
  postcomp⋆PshHomᴰⱽ-Iso
    : (βⱽ : PshIsoⱽ Qᴰ Rᴰ)
    → ∀ {α : PshHom P Q}
    → Iso (PshHomᴰ α Pᴰ Qᴰ) (PshHomᴰ α Pᴰ Rᴰ)
  postcomp⋆PshHomᴰⱽ-Iso βⱽ .Iso.fun = _⋆PshHomᴰⱽ βⱽ .fst
  postcomp⋆PshHomᴰⱽ-Iso βⱽ .Iso.inv = _⋆PshHomᴰⱽ invPshIsoⱽ βⱽ .fst
  postcomp⋆PshHomᴰⱽ-Iso βⱽ .Iso.sec αᴰ =
    ⋆PshHomAssocᴰⱽⱽ _ _ _
    ∙ cong (αᴰ ⋆PshHomᴰⱽ_) (PshIsoⱽ→PshIsoⱽ' _ _ βⱽ .snd .snd .snd)
    ∙ ⋆PshHomIdRᴰⱽ αᴰ
  postcomp⋆PshHomᴰⱽ-Iso βⱽ .Iso.ret αᴰ = ⋆PshHomAssocᴰⱽⱽ _ _ _
    ∙ cong (αᴰ ⋆PshHomᴰⱽ_) (PshIsoⱽ→PshIsoⱽ' _ _ βⱽ .snd .snd .fst)
    ∙ ⋆PshHomIdRᴰⱽ αᴰ

open Iso
open UniversalElementⱽ
module _ (C : Category ℓC ℓC') (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') (ℓP ℓPᴰ : Level) where
  private
    module PSHᴰ = Fibers (PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ)

  module _ {P : Presheaf C ℓP}{Q : Presheaf C ℓP}
    {Pᴰ : Presheafᴰ P Cᴰ ℓPᴰ}{Qᴰ : Presheafᴰ Q Cᴰ ℓPᴰ}{Rᴰ : Presheafᴰ Q Cᴰ ℓPᴰ}
    where
    private
      module Pᴰ = PresheafᴰNotation Pᴰ
      module Rᴰ = PresheafᴰNotation Rᴰ
    module _ {α : PshHom P Q} where
      opaque
        unfolding hSetReasoning.reind
        ⋆PshHomᴰⱽ≡ : (αᴰ : PshHomᴰ α Pᴰ Qᴰ)(βᴰ : PshHomⱽ Qᴰ Rᴰ)
          → αᴰ ⋆PshHomᴰⱽ βᴰ ≡ (αᴰ PSHᴰ.⋆ᴰⱽ βᴰ)
        ⋆PshHomᴰⱽ≡ αᴰ βᴰ = sym (fromPathP (makePshHomᴰPathP (αᴰ PSHᴰ.⋆ᴰ βᴰ) (αᴰ ⋆PshHomᴰⱽ βᴰ) _
          (funExt λ pᴰ → Rᴰ.rectify $ Rᴰ.≡out refl)))
  module _ {P : Presheaf C ℓP}{Q : Presheaf C ℓP}{R : Presheaf C ℓP}
    (α : PshHom Q P)(β : PshHom R Q)(Pᴰ : Presheafᴰ P Cᴰ ℓPᴰ)(Rᴰ : Presheafᴰ R Cᴰ ℓPᴰ)(βᴰ : PshHomᴰ β Rᴰ (reind α Pᴰ))
    where
    private
      module Pᴰ = PresheafᴰNotation Pᴰ
      module α*Pᴰ = PresheafⱽNotation
        (reindYo {C = PRESHEAF C _}{Cᴰ = PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ} α (PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ [-][-, Pᴰ ]))

    opaque
      unfolding hSetReasoning.reind
      reind⋆ᴰ≡⋆PshHomᴰ : βᴰ α*Pᴰ.⋆ᴰ (idPshHomᴰ ⋆PshHomᴰ reind-π) ≡ (βᴰ ⋆PshHomᴰ idPshHomᴰ) ⋆PshHomᴰ reind-π
      reind⋆ᴰ≡⋆PshHomᴰ = fromPathP (makePshHomᴰPathP _ _ _ (funExt λ rᴰ → Pᴰ.rectify $ Pᴰ.≡out $ refl ))

      reind⋆ᴰⱽ≡⋆PshHomᴰ : βᴰ α*Pᴰ.⋆ᴰⱽ (idPshHomᴰ ⋆PshHomᴰ reind-π) ≡ (βᴰ ⋆PshHomᴰⱽ idPshHomᴰ) ⋆PshHomᴰ reind-π
      reind⋆ᴰⱽ≡⋆PshHomᴰ = fromPathP (reind⋆ᴰ≡⋆PshHomᴰ ◁ (makePshHomᴰPathP _ _ _ (funExt λ rᴰ → Pᴰ.rectify $ Pᴰ.≡out $
        refl)))

  module _ {P : Presheaf C ℓP}{R : Presheaf C ℓP}
    {Pᴰ : Presheafᴰ P Cᴰ ℓPᴰ}{Qᴰ : Presheafᴰ P Cᴰ ℓPᴰ}{Rᴰ : Presheafᴰ R Cᴰ ℓPᴰ}
    where
    private
      module Pᴰ = PresheafᴰNotation Pᴰ
      module Rᴰ = PresheafᴰNotation Rᴰ
    module _ {β : PshHom P R} where

      opaque
        unfolding hSetReasoning.reind
        ⋆PshHomⱽᴰ≡ : (αⱽ : PshHomⱽ Pᴰ Qᴰ)(βᴰ : PshHomᴰ β Qᴰ Rᴰ)
          → αⱽ ⋆PshHomⱽᴰ βᴰ ≡ (αⱽ PSHᴰ.⋆ⱽᴰ βᴰ)
        ⋆PshHomⱽᴰ≡ αⱽ βᴰ = sym (fromPathP (makePshHomᴰPathP (αⱽ PSHᴰ.⋆ᴰ βᴰ) (αⱽ ⋆PshHomⱽᴰ βᴰ) _
          (funExt λ pᴰ → Rᴰ.rectify $ Rᴰ.≡out refl)))


  -- TODO only use opacity for the proofs
  opaque
    unfolding hSetReasoning.reind
    -- TODO: need Iso (PshHomᴰ α) (NatTransᴰ (PH→NT α)) and vice-versa
    PRESHEAFᴰ-Terminalsⱽ : Terminalsⱽ (PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ)
    PRESHEAFᴰ-Terminalsⱽ P .vertexⱽ = LiftPshᴰ UnitPshᴰ ℓPᴰ
    PRESHEAFᴰ-Terminalsⱽ P .elementⱽ = _
    PRESHEAFᴰ-Terminalsⱽ P .universalⱽ .fst _ = UnitPshᴰ-introᴰ ⋆PshHomᴰⱽ LiftHomⱽ UnitPshᴰ
    PRESHEAFᴰ-Terminalsⱽ P .universalⱽ .snd .fst = λ _ → refl
    PRESHEAFᴰ-Terminalsⱽ P .universalⱽ .snd .snd = λ αᴰ →
      isoFunInjective (postcomp⋆PshHomᴰⱽ-Iso (invPshIsoⱽ (LiftIsoⱽ UnitPshᴰ))) _ _ (isoInvInjective UnitPshᴰ-UMP _ _ refl)

    PRESHEAFᴰ-BinProductsⱽ : BinProductsⱽ (PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ)
    PRESHEAFᴰ-BinProductsⱽ P Pᴰ,Qᴰ .vertexⱽ = Pᴰ,Qᴰ .fst ×ⱽPsh Pᴰ,Qᴰ .snd
    PRESHEAFᴰ-BinProductsⱽ P Pᴰ,Qᴰ .elementⱽ =
      ×ⱽ-π₁ {Pᴰ = Pᴰ,Qᴰ .fst}{Qᴰ = Pᴰ,Qᴰ .snd}
      , ×ⱽ-π₂ {Pᴰ = Pᴰ,Qᴰ .fst}{Qᴰ = Pᴰ,Qᴰ .snd}
    PRESHEAFᴰ-BinProductsⱽ P Pᴰ,Qᴰ .universalⱽ .fst αᴰβᴰ =
      ×ⱽ-introᴰ (αᴰβᴰ .fst) (αᴰβᴰ .snd)
    PRESHEAFᴰ-BinProductsⱽ P Pᴰ,Qᴰ .universalⱽ .snd .fst αᴰβᴰ =
    -- TODO: figure out how to make this faster
      ΣPathP (sym (⋆PshHomᴰⱽ≡ (×ⱽ-introᴰ (αᴰβᴰ .fst) (αᴰβᴰ .snd)) (×ⱽ-π₁ {Pᴰ = Pᴰ,Qᴰ .fst}{Qᴰ = Pᴰ,Qᴰ .snd})) ∙ (cong fst $ ×ⱽPsh-UMPᴰ {Qᴰ = Pᴰ,Qᴰ .fst}{Rᴰ = Pᴰ,Qᴰ .snd} .ret (αᴰβᴰ .fst , αᴰβᴰ .snd))
      , sym (⋆PshHomᴰⱽ≡ (×ⱽ-introᴰ (αᴰβᴰ .fst) (αᴰβᴰ .snd)) (×ⱽ-π₂ {Pᴰ = Pᴰ,Qᴰ .fst}{Qᴰ = Pᴰ,Qᴰ .snd})) ∙ (cong snd $ ×ⱽPsh-UMPᴰ {Qᴰ = Pᴰ,Qᴰ .fst}{Rᴰ = Pᴰ,Qᴰ .snd} .ret (αᴰβᴰ .fst , αᴰβᴰ .snd) ))
    PRESHEAFᴰ-BinProductsⱽ P Pᴰ,Qᴰ .universalⱽ .snd .snd αᴰ =
      isoFun≡ (×ⱽPsh-UMPᴰ {Qᴰ = Pᴰ,Qᴰ .fst} {Rᴰ = Pᴰ,Qᴰ .snd})
        (ΣPathP ((sym (⋆PshHomᴰⱽ≡ αᴰ _)) , (sym (⋆PshHomᴰⱽ≡ αᴰ _))))

    PRESHEAFᴰ-isFibration : isFibration (PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ)
    PRESHEAFᴰ-isFibration {P} Pᴰ {Q} α .vertexⱽ = reind α Pᴰ
    PRESHEAFᴰ-isFibration {P} Pᴰ {Q} α .elementⱽ = idPshHomᴰ ⋆PshHomᴰ reind-π
    PRESHEAFᴰ-isFibration {P} Pᴰ {Q} α .universalⱽ {R} {Rᴰ} {β} .fst = reind-introᴰ
    PRESHEAFᴰ-isFibration {P} Pᴰ {Q} α .universalⱽ {R} {Rᴰ} {β} .snd =
      (λ βαᴰ →
      (reind-introᴰ βαᴰ α*Pᴰ.⋆ᴰⱽ (idPshHomᴰ ⋆PshHomᴰ reind-π))
        ≡⟨ lem (reind-introᴰ βαᴰ) ⟩
      (reind-introᴰ βαᴰ ⋆PshHomᴰ reind-π)
        ≡⟨ reind-UMP {α = β}{β = α} .ret βαᴰ ⟩
      βαᴰ ∎)
      , (λ βᴰ →
        cong reind-introᴰ (lem βᴰ)
        ∙ reind-UMP .sec βᴰ)
      where
        module α*Pᴰ = PresheafⱽNotation
          (reindYo {C = PRESHEAF C _}{Cᴰ = PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ} α (PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ [-][-, Pᴰ ]))
        module Pᴰ = PresheafᴰNotation Pᴰ

        lem : ∀ (βᴰ : PshHomᴰ β Rᴰ (reind α Pᴰ))
          → (βᴰ α*Pᴰ.⋆ᴰⱽ (idPshHomᴰ ⋆PshHomᴰ reind-π))
            ≡ βᴰ ⋆PshHomᴰ reind-π
        lem βᴰ = reind⋆ᴰⱽ≡⋆PshHomᴰ _ _ _ _ _
          ∙ cong (_⋆PshHomᴰ reind-π) (⋆PshHomIdRᴰⱽ βᴰ)

    PRESHEAFᴰ-CCⱽ : CartesianCategoryⱽ (PRESHEAF C ℓP)
      (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓC ℓC') ℓCᴰ) ℓCᴰ') (ℓ-suc ℓP)) (ℓ-suc ℓPᴰ))
      (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓC ℓC') ℓCᴰ) ℓCᴰ') ℓP) ℓPᴰ)
    PRESHEAFᴰ-CCⱽ .CartesianCategoryⱽ.Cᴰ = PRESHEAFᴰ' Cᴰ ℓP ℓPᴰ
    PRESHEAFᴰ-CCⱽ .CartesianCategoryⱽ.termⱽ = PRESHEAFᴰ-Terminalsⱽ
    PRESHEAFᴰ-CCⱽ .CartesianCategoryⱽ.bpⱽ = PRESHEAFᴰ-BinProductsⱽ
    PRESHEAFᴰ-CCⱽ .CartesianCategoryⱽ.cartesianLifts = PRESHEAFᴰ-isFibration

-- For exponentials need to implement ⇒PshLargeⱽ
--   PRESHEAFᴰ-Exponentialsⱽ : Exponentialsⱽ (PRESHEAFᴰ Cᴰ ℓS ℓS') {!!} {!!}
--   PRESHEAFᴰ-Exponentialsⱽ = {!!}