{-# OPTIONS --lossy-unification #-}
module Cubical.Categories.LocallySmall.Displayed.Presheaf.GloballySmall.IntoFiberCategory.Base where

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

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

import Cubical.Categories.Category.Base as SmallCat
import Cubical.Categories.Displayed.Base as SmallCatᴰ
import Cubical.Categories.Presheaf.Base as SmallPsh
import Cubical.Categories.Displayed.Presheaf.Base as SmallPshᴰ
import Cubical.Categories.Functor.Base as SmallFunctor
import Cubical.Categories.Displayed.Functor as SmallFunctorᴰ

open import Cubical.Categories.LocallySmall.Variables
open import Cubical.Categories.LocallySmall.Category.Base
open import Cubical.Categories.LocallySmall.Category.Small
open import Cubical.Categories.LocallySmall.Instances.Level
open import Cubical.Categories.LocallySmall.Instances.Functor.IntoFiberCategory
open import Cubical.Categories.LocallySmall.Functor using (_∘F_ ; _^opF)
import Cubical.Categories.LocallySmall.Functor as LocallySmallF
open import Cubical.Categories.LocallySmall.Presheaf.GloballySmall.IntoFiberCategory.Base

open import Cubical.Categories.LocallySmall.Displayed.Category
open import Cubical.Categories.LocallySmall.Displayed.Instances.Sets.Base
open import Cubical.Categories.LocallySmall.Displayed.Instances.Functor.IntoFiberCategory
open import Cubical.Categories.LocallySmall.Displayed.Functor.Base using (_∘Fᴰ_)
import Cubical.Categories.LocallySmall.Displayed.Functor.Base as LocallySmallFᴰ
open import Cubical.Categories.LocallySmall.Displayed.Functor.Properties using (_^opFᴰ)
import Cubical.Categories.LocallySmall.Displayed.Functor.Properties as LocallySmallFᴰ
open import Cubical.Categories.LocallySmall.Displayed.Section.Base
open import Cubical.Categories.LocallySmall.Displayed.Constructions.Total
open import Cubical.Categories.LocallySmall.Displayed.Constructions.Weaken
open import Cubical.Categories.LocallySmall.Displayed.Constructions.BinProduct.Base
open import Cubical.Categories.LocallySmall.Displayed.NaturalTransformation.IntoFiberCategory.Base
open import Cubical.Categories.LocallySmall.Displayed.NaturalTransformation.IntoFiberCategory.Eq

open Σω
open Liftω
open LocallySmallF.Functor
open LocallySmallFᴰ.Functorᴰ

private
  module SET = CategoryᴰNotation SET
  module SETᴰ = SmallFibersᴰNotation SETᴰ

module _ {C : SmallCategory ℓC ℓC'} (P : Presheaf C ℓP) (Cᴰ : SmallCategoryᴰ C ℓCᴰ ℓCᴰ') where
  private
    module C = SmallCategory C
    module Cᴰ = SmallCategoryᴰ Cᴰ
    module CᴰNotation = CategoryᴰNotation (Cᴰ.catᴰ)

  open NatTransᴰDefs (Cᴰ ^opsmallᴰ) (weaken LEVEL LEVEL) SET SETᴰ
  open FunctorEqᴰDefs (Cᴰ ^opsmallᴰ) (weaken LEVEL LEVEL) SET SETᴰ

  Presheafᴰ : Level → Typeω
  Presheafᴰ ℓPᴰ = FunctorEqᴰ Eq.refl (λ _ _ → Eq.refl) P (liftω ℓPᴰ)

  module _ (Pᴰ : Presheafᴰ ℓPᴰ) where
    ∫P : Presheaf Cᴰ.∫Csmall (ℓ-max ℓP ℓPᴰ)
    ∫P = ΣF ℓP ℓPᴰ ∘F ∫F Pᴰ ∘F F
      where
      F : LocallySmallF.Functor
        (SmallCategory.cat (Cᴰ.∫Csmall ^opsmall))
        (Categoryᴰ.∫C (SmallCategoryᴰ.catᴰ (Cᴰ ^opsmallᴰ)))
      F .F-ob = λ z → liftω (z .lowerω .fst) , liftω (z .lowerω .snd)
      F .F-hom = λ z → z
      F .F-id = refl
      F .F-seq = λ _ _ → refl

module _ {C : SmallCategory ℓC ℓC'} (Cᴰ : SmallCategoryᴰ C ℓCᴰ ℓCᴰ') where
  private
    PSH = PRESHEAF C
    LEVEL×PSH = weaken LEVEL LEVEL ×ᴰ PRESHEAF C
    module C = SmallCategory C
    module Cᴰ = SmallCategoryᴰ Cᴰ
    module LEVEL×PSH = CategoryᴰNotation LEVEL×PSH

  open FunctorEqᴰDefs (Cᴰ ^opsmallᴰ) (weaken LEVEL LEVEL) SET SETᴰ

  -- PRESHEAFᴰ is displayed over LEVEL×PSH
  -- where
  -- LEVEL×PSH is the fiberwise product of the category of
  -- levels weakened over itself and the displayed
  -- category of globally small presheaves
  --
  --         PRESHEAFᴰ
  --             |
  --             v
  --    /  LEVEL × PRESHEAF \
  --  ∫ |        |          |
  --    |        v          |
  --    \      LEVEL        /
  PRESHEAFᴰ : Categoryᴰ LEVEL×PSH.∫C _ _
  PRESHEAFᴰ = FUNCTOR-EQᴰ (Cᴰ ^opsmallᴰ) (weaken LEVEL LEVEL) SET SETᴰ
    Eq.refl (λ _ _ _ _ → Eq.refl)

module _ {C : SmallCategory ℓC ℓC'} (Cᴰ : SmallCategoryᴰ C ℓCᴰ ℓCᴰ') where
  private
    PSH = PRESHEAF C
    LEVEL×PSH = weaken LEVEL LEVEL ×ᴰ PRESHEAF C
    module C = SmallCategory C
    module Cᴰ = SmallCategoryᴰ Cᴰ
    module LEVEL×PSH = CategoryᴰNotation LEVEL×PSH

  private
    module PSHᴰ = CategoryᴰNotation (PRESHEAFᴰ Cᴰ)
    module PSHISOᴰ = CategoryᴰNotation PSHᴰ.ISOCᴰ

  module _ {P : Presheaf C ℓP}{Q : Presheaf C ℓQ}
    (α : PshHom P Q)
    (Pᴰ : Presheafᴰ P Cᴰ ℓPᴰ) (Qᴰ : Presheafᴰ Q Cᴰ ℓQᴰ) where

    PshHomᴰ : Type _
    PshHomᴰ = PSHᴰ.Hom[ _ , _ , α ][ Pᴰ , Qᴰ ]

  module _ {D : SmallCategory ℓD ℓDᴰ'} {Dᴰ : SmallCategoryᴰ D ℓDᴰ ℓDᴰ'}
    where
    private
      module D = SmallCategory D
      module Dᴰ = SmallCategoryᴰ Dᴰ

    module _ {F : LocallySmallF.Functor (C.cat) (D.cat)}
      {P : Presheaf C ℓP} {Q : Presheaf D ℓQ}
      (α : PshHet F P Q)
      (Fᴰ : LocallySmallFᴰ.Functorᴰ F Cᴰ.catᴰ Dᴰ.catᴰ)
      (Pᴰ : Presheafᴰ P Cᴰ ℓPᴰ) (Qᴰ : Presheafᴰ Q Dᴰ ℓQᴰ) where
      PshHetᴰ : Type _
      PshHetᴰ = PshHomᴰ α Pᴰ (Qᴰ ∘Fᴰ (Fᴰ ^opFᴰ))