open import Cat.Displayed.Base
open import Cat.Prelude

module Cat.Displayed.Cartesian
{o β oβ² ββ²} {B : Precategory o β} (E : Displayed B oβ² ββ²) where

open Precategory B
open Displayed E


# Cartesian Morphisms and Fibrationsπ

record Cartesian {a b x y} (f : Hom a b)
(fβ² : Hom[ f ] x y) : Type (o β β β oβ² β ββ²) where
field
universal : β {u uβ²} (m : Hom u a) β (hβ² : Hom[ f β m ] uβ² y) β Hom[ m ] uβ² x
commutes  : β {u uβ²} (m : Hom u a) β (hβ² : Hom[ f β m ] uβ² y)
β fβ² ββ² universal m hβ² β‘ hβ²
unique    : β {u uβ²} {m : Hom u a} β {hβ² : Hom[ f β m ] uβ² y}
β (mβ² : Hom[ m ] uβ² x) β fβ² ββ² mβ² β‘ hβ² β mβ² β‘ universal m hβ²

record Cartesian-lift {x y} (f : Hom x y) (yβ² : Ob[ y ]) : Type (o β β β oβ² β ββ²) where
field
{xβ²}       : Ob[ x ]
lifting   : Hom[ f ] xβ² yβ²
cartesian : Cartesian f lifting

record Cartesian-fibration : Type (o β β β oβ² β ββ²) where
field
has-lift : β {x y} (f : Hom x y) β (yβ² : Ob[ y ]) β Cartesian-lift f yβ²