{-# OPTIONS --lossy-unification #-}
-- Reindexing a Presheaf by a Functor.

-- given presheaf Q on D and functor F : C → D we can reindex Q to be
-- a presheaf F* Q on C. This is just precomposition Q ∘ F^op

-- This corresponds to something wacky like "presheaves are a
-- 2-presheaf on the 2-category Cat".
module Cubical.Categories.Presheaf.Constructions.Reindex where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.More
open import Cubical.Foundations.Transport hiding (pathToIso)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Isomorphism.More
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure

open import Cubical.Functions.FunExtEquiv

open import Cubical.Reflection.RecordEquiv.More
open import Cubical.Data.Sigma
import Cubical.Data.Equality as Eq

open import Cubical.Categories.Category renaming (isIso to isIsoC)
open import Cubical.Categories.Bifunctor
open import Cubical.Categories.Constructions.Elements
open import Cubical.Categories.Constructions.Lift
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.Sets.More
open import Cubical.Categories.Limits
open import Cubical.Categories.NaturalTransformation hiding (_∘ˡ_; _∘ˡⁱ_)
open import Cubical.Categories.Presheaf.Base
open import Cubical.Categories.Presheaf.More
open import Cubical.Categories.Presheaf.Morphism.Alt
open import Cubical.Categories.Presheaf.Representable
open import Cubical.Categories.Presheaf.Properties renaming (PshIso to PshIsoLift)
open import Cubical.Categories.Profunctor.General
open import Cubical.Categories.Profunctor.Constructions.Extension
open import Cubical.Categories.Presheaf.Constructions.Tensor

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

open Category
open Contravariant -- Grothendieck construction for presheaves
open Functor
open NatTrans
open NatIso
open PshHom
open PshIso
open UniversalElement

-- Whiskering
module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
  -- TODO: define this as a universe-polymorphic functor once we have that
  -- reindPsh : Functor C D → Functor (Presheaf D) (Presheaf C)
  reindPsh : (F : Functor C D) (Q : Presheaf D ℓQ) → Presheaf C ℓQ
  reindPsh F Q = Q ∘F (F ^opF)

  reindPshF : (F : Functor C D) → Functor (PresheafCategory D ℓQ) (PresheafCategory C ℓQ)
  reindPshF F = precomposeF (SET _) (F ^opF)

  -- This is just whiskering
  reindPshHom : {P : Presheaf D ℓP}{Q : Presheaf D ℓQ}
    → (F : Functor C D) (α : PshHom P Q)
    → PshHom (reindPsh F P) (reindPsh F Q)
  reindPshHom F α .N-ob c = α .N-ob _
  reindPshHom F α .N-hom c c' f = α .N-hom _ _ _

  -- TODO: This is a consequence of functoriality...
  reindPshIso : {P : Presheaf D ℓP}{Q : Presheaf D ℓQ}
    → (F : Functor C D) (α : PshIso P Q)
    → PshIso (reindPsh F P) (reindPsh F Q)
  reindPshIso F α .trans = reindPshHom F (α .trans)
  reindPshIso F α .nIso x .fst = α .nIso _ .fst
  reindPshIso F α .nIso x .snd .fst = α .nIso _ .snd .fst
  reindPshIso F α .nIso x .snd .snd = α .nIso _ .snd .snd

  -- this is right-whiskering
  reindNatTransPsh :
    {F G : Functor C D}
    → (α : NatTrans G F) (P : Presheaf D ℓP)
    → PshHom (reindPsh F P) (reindPsh G P)
  reindNatTransPsh α P = pshhom (λ c p → α.N-ob c P.⋆ p) λ _ _ f p →
    sym (P.⋆Assoc _ _ _) ∙ P.⟨ sym $ α.N-hom f ⟩⋆⟨⟩ ∙ P.⋆Assoc _ _ _
    where
      module α = NatTrans α
      module P = PresheafNotation P

  reindNatIsoPsh :
    {F G : Functor C D}
    → (α : NatIso F G) (P : Presheaf D ℓP)
    → PshIso (reindPsh F P) (reindPsh G P)
  reindNatIsoPsh α P .trans = reindNatTransPsh (symNatIso α .trans) P
  reindNatIsoPsh α P .nIso x .fst = reindNatTransPsh (α .trans) P .N-ob _
  reindNatIsoPsh α P .nIso x .snd =
    (λ p → sym (P.⋆Assoc _ _ _) ∙ P.⟨ α .nIso x .isIsoC.sec ⟩⋆⟨⟩ ∙ P.⋆IdL p)
    , λ p → sym (P.⋆Assoc _ _ _) ∙ P.⟨ α .nIso x .isIsoC.ret ⟩⋆⟨⟩ ∙ P.⋆IdL p
    where
      module P = PresheafNotation P

  PshHet : (F : Functor C D) (P : Presheaf C ℓP) (Q : Presheaf D ℓQ) → Type _
  PshHet F P Q = PshHom P (reindPsh F Q)

  Functor→PshHet : (F : Functor C D) (c : C .ob)
    → PshHet F (C [-, c ]) (D [-, F ⟅ c ⟆ ])
  Functor→PshHet F c .N-ob _ = F .F-hom
  Functor→PshHet F c .N-hom _ _ = F .F-seq

  module _ {F : Functor C D}{P : Presheaf C ℓP}{Q : Presheaf D ℓQ}
    (α : PshHet F P Q)
    where
    private
      module P = PresheafNotation P
      module Q = PresheafNotation Q

    becomesUniversal : ∀ (v : C .ob) (e : P.p[ v ]) → Type _
    becomesUniversal v e = isUniversal D Q (F ⟅ v ⟆) (α .N-ob v e)

    preservesUniversalElement : UniversalElement C P → Type _
    preservesUniversalElement ue = becomesUniversal (ue .vertex) (ue .element)

    preservesUniversalElements = ∀ ue → preservesUniversalElement ue

    becomesUniversal→UniversalElement :
      ∀ {v e} → becomesUniversal v e → UniversalElement D Q
    becomesUniversal→UniversalElement isUniv .vertex = _
    becomesUniversal→UniversalElement isUniv .element = _
    becomesUniversal→UniversalElement isUniv .universal = isUniv

    preservesUniversalElement→UniversalElement :
      ∀ ue → preservesUniversalElement ue → UniversalElement D Q
    preservesUniversalElement→UniversalElement ue preservesUE
      = becomesUniversal→UniversalElement preservesUE

    ∫ᴾPshHet : Functor (∫ᴾ P) (∫ᴾ Q)
    ∫ᴾPshHet .F-ob (x , e) = F ⟅ x ⟆ , α .N-ob x e
    ∫ᴾPshHet .F-hom (f , fe≡e') = (F ⟪ f ⟫) ,
      (sym $ α .N-hom _ _ _ _) ∙ cong (α .N-ob _) fe≡e'
    ∫ᴾPshHet .F-id =
      Σ≡Prop (λ _ → Q.isSetPsh _ _ ) (F .F-id)
    ∫ᴾPshHet .F-seq (f , _) (g , _) =
      Σ≡Prop (λ _ → Q.isSetPsh _ _ ) (F .F-seq f g)

    -- If a presheaf preserves any universal element then it preserves
    -- all of them since universal elements are unique up to unique
    -- isomorphism. This is for free if the category is univalent
    -- because in that case UniversalElement C P is a Prop.

    -- This lemma, like other applications of Yoneda should be taken as
    -- an indication that it is probably fine to build the library
    -- around the seemingly weaker notion of preservesUniversalElement
    -- and push uses of this lemma to users rather than to pervasively
    -- use this in the library itself. YMMV
    preservesUniversalElement→PreservesUniversalElements :
      ∀ ue → preservesUniversalElement ue → preservesUniversalElements
    preservesUniversalElement→PreservesUniversalElements ue preservesUE ue' =
      isTerminalToIsUniversal D Q $
        preserveAnyTerminal→PreservesTerminals
          (∫ᴾ P)
          (∫ᴾ Q)
          ∫ᴾPshHet
          (universalElementToTerminalElement C P ue)
          (isUniversalToIsTerminal D Q _ _ preservesUE)
          (universalElementToTerminalElement C P ue')

-- Functoriality of reindexing in F
reindPshId≅ : {C : Category ℓC ℓC'} (P : Presheaf C ℓP)
  → PshIso P (reindPsh Id P)
reindPshId≅ P = eqToPshIso (reindPsh Id P) Eq.refl Eq.refl

-- -- TODO
reindPsh∘F≅ :
  {C : Category ℓC ℓC'}
  {D : Category ℓD ℓD'}
  {E : Category ℓE ℓE'}
  (F : Functor C D)
  (G : Functor D E)
  (P : Presheaf E ℓP)
  → PshIso (reindPsh F (reindPsh G P)) (reindPsh (G ∘F F) P)
reindPsh∘F≅ F G P = eqToPshIso (reindPsh (G ∘F F) P) Eq.refl Eq.refl

module _ {C : Category ℓC ℓC'}
  {P : Presheaf C ℓP}{Q : Presheaf C ℓQ}
  where
  PshHom→PshHet : PshHom P Q → PshHet Id P Q
  PshHom→PshHet α = α ⋆PshHom reindPshId≅ Q .trans
module _ {C : Category ℓC ℓC'} {P : Presheaf C ℓP} where
  idPshHet : PshHet Id P P
  idPshHet = PshHom→PshHet idPshHom

module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
  {E : Category ℓE ℓE'}{F : Functor C D}{G : Functor D E}
  {P : Presheaf C ℓP}{Q : Presheaf D ℓQ}{R : Presheaf E ℓR}
  where
  _⋆PshHet_ : PshHet F P Q → PshHet G Q R → PshHet (G ∘F F) P R
  α ⋆PshHet β = α ⋆PshHom reindPshHom F β ⋆PshHom reindPsh∘F≅ F G R .trans

module _ {B : Category ℓB ℓB'}{C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
  -- reindPsh F (c ↦ P(c,d) ⊗[ d ] Q(d,*))
  -- ≅ b ↦ P(F b, d) ⊗[ d ] Q(d, *)
  reindPsh-⊗ : (F : Functor B C) (P : Bifunctor (C ^op) D (SET ℓR)) (Q : Presheaf D ℓQ)
    → PshIso (reindPsh F (ext P ⟅ Q ⟆))
             (ext ((CurriedToBifunctorL (reindPshF F ∘F CurryBifunctorL P))) ⟅ Q ⟆)
  reindPsh-⊗ F P Q = pshiso (pshhom
    (λ b → P⊗Q.rec extF*PQ.isSetPsh F*P⊗Q._,⊗_ F*P⊗Q.swap)
    λ b b' f → P⊗Q.ind (λ _ → extF*PQ.isSetPsh _ _) (λ _ _ → refl))
    λ b → (F*P⊗Q.rec F*extPQ.isSetPsh P⊗Q._,⊗_ P⊗Q.swap)
    , F*P⊗Q.ind (λ _ → extF*PQ.isSetPsh _ _) (λ _ _ → refl)
    , P⊗Q.ind (λ _ → extPQ.isSetPsh _ _) λ _ _ → refl
    where
      F*P = CurriedToBifunctorL (reindPshF F ∘F CurryBifunctorL P)
      module F*extPQ = PresheafNotation (reindPsh F (ext P ⟅ Q ⟆))
      module extPQ = PresheafNotation (ext P ⟅ Q ⟆)
      module extF*PQ = PresheafNotation (ext F*P ⟅ Q ⟆)
      module P⊗Q = ext-⊗ P Q
      module F*P⊗Q = ext-⊗ F*P Q

  -- reindPsh F (c ↦ ∀[ d ] P(d,c) → Q(d,*))
  -- ≅ (b ↦ ∀[ d ] P(d,F b) → Q(d,*))
  reindPsh-PshHom : (F : Functor B C) (P : Bifunctor (D ^op) C (SET ℓR)) (Q : Presheaf D ℓQ)
    → PshIso (reindPsh F $ appR (PshHomBif ∘Fl (CurryBifunctorL P ^opF)) Q)
             (appR (PshHomBif ∘Fl ((CurryBifunctorL (P ∘Fr F)) ^opF) ) Q)
  reindPsh-PshHom F P Q = pshiso (pshhom (λ b α → pshhom (α .N-ob) (α .N-hom)) λ _ _ f α → makePshHomPath refl)
    λ b → (λ β → pshhom (β .N-ob) (β .N-hom))
    , (λ α → makePshHomPath refl)
    , (λ β → makePshHomPath refl)
module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
  reindPshF-cocont : (F : Functor C D)
    → CoContinuous (reindPshF F)
  reindPshF-cocont F Q =
    -- F* Q
    reindPshIso F (CoYoneda Q)
    -- F* ◇Q
    ⋆PshIso reindPsh-⊗ F (HomBif D) Q
    -- ◇ (F* Q)