{-# OPTIONS --lossy-unification #-}
module Cubical.Categories.Displayed.Fibration.Manual where

open import Cubical.Data.Sigma

open import Cubical.Categories.Category.Base hiding (isIso)
open import Cubical.Categories.Instances.Fiber

open import Cubical.Categories.Displayed.Base
open import Cubical.Categories.Displayed.Instances.Sets.Base
open import Cubical.Categories.Displayed.Presheaf.CartesianLift.Manual
  using () renaming (
    CartesianLift to PshᴰCartesianLift
  ; isFibration to PshᴰisFibration) public

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


module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
  private
    module Cᴰ = Fibers Cᴰ
    module C = Category C

  -- The Cartesian lifting of a displayed object yᴰ along f
  -- is precisely the data that Cᴰ [-][-, yᴰ ] has a
  -- Cartesian lift (of displayed presheaves) along
  -- f (viewed as an element of C [-, y ])
  CartesianLift :
    {x y : C.ob} (yᴰ : Cᴰ.ob[ y ]) (f : C [ x , y ]) → Type _
  CartesianLift yᴰ f = PshᴰCartesianLift f (Cᴰ [-][-, yᴰ ])

  isFibration : Type _
  isFibration =
    ∀ {c : C.ob} (cᴰ : Cᴰ.ob[ c ]) → PshᴰisFibration (Cᴰ [-][-, cᴰ ])