module Cat.Displayed.Instances.Objects
  {o β„“ o' β„“'} {B : Precategory o β„“}
  (E : Displayed B o' β„“')

The fibration of objectsπŸ”—

Let be a fibration. Its fibration of objects is the wide subcategory spanned by the cartesian morphisms. The idea behind the name is that we’ve kept all the objects in but removed all the interesting morphisms: all we’ve kept are the ones that witness changes-of-base.

Objects : Displayed B o' (o βŠ” β„“ βŠ” o' βŠ” β„“')
Objects .Displayed.Ob[_] x = Ob[ x ]
Objects .Displayed.Hom[_] f x' y'   = Cartesian-morphism E f x' y'
Objects .Displayed.Hom[_]-set _ _ _ = Cartesian-morphism-is-set E
Objects'  = idcart E
Objects .Displayed._∘'_ = _∘cart_ E
Objects .Displayed.idr' _       = Cartesian-morphism-pathp E (idr' _)
Objects .Displayed.idl' _       = Cartesian-morphism-pathp E (idl' _)
Objects .Displayed.assoc' _ _ _ = Cartesian-morphism-pathp E (assoc' _ _ _)

We have an evident forgetful fibred functor from the object fibration back to

Objects-forget : Vertical-fibred-functor Objects E
Objects-forget .vert .Fβ‚€' x = x
Objects-forget .vert .F₁' f' = f' .hom'
Objects-forget .vert .F-id' = refl
Objects-forget .vert .F-∘' = refl
Objects-forget .F-cartesian f' _ = f' .cartesian

Since the object fibration only has Cartesian morphisms from we can prove that it consists entirely of Cartesian maps. This is not immediate, since to include the β€œuniversal” map, we must prove that it too is Cartesian; but that follows from the pasting law for Cartesian squares.

  : βˆ€ {x y x' y'} {f : Hom x y} (f' : Cartesian-morphism E f x' y')
  β†’ is-cartesian Objects f f'
Objects-cartesian f' = cart where
  open is-cartesian

  cart : is-cartesian _ _ _
  cart .universal m h' = cart-paste E f' h'
  cart .commutes m h' =
    Cartesian-morphism-pathp E (f' .cartesian .commutes m (h' .hom'))
  cart .unique m' p =
    Cartesian-morphism-pathp E (f' .cartesian .unique (hom' m') (ap hom' p))

If is a fibration, then its fibration of objects is a a right fibration, by the preceding result. This means the fibres of the object fibration are groupoids.

Objects-fibration : Cartesian-fibration E β†’ Cartesian-fibration Objects
Objects-fibration fib .Cartesian-fibration.has-lift f y' = cart-lift where
  open Cartesian-fibration fib

  cart-lift : Cartesian-lift Objects f y'
  cart-lift .Cartesian-lift.x' = has-lift.x' f y'
  cart-lift .Cartesian-lift.lifting .hom' = has-lift.lifting f y'
  cart-lift .Cartesian-lift.lifting .cartesian = has-lift.cartesian f y'
  cart-lift .Cartesian-lift.cartesian = Objects-cartesian _

Objects-right-fibration : Cartesian-fibration E β†’ Right-fibration Objects
Objects-right-fibration fib = Objects-fibration fib
Objects-right-fibration fib .Right-fibration.cartesian = Objects-cartesian

The core of a fibrationπŸ”—

The fibration of objects is the relative analog of the core of a category, sharing its universal property. Rather than a groupoid, suppose we have a right fibration and a fibred functor to complete the analogy, we show factors through fibration of objects.

    : (F : Vertical-fibred-functor R E)
    β†’ Vertical-fibred-functor R Objects
  Objects-universal F .vert .Fβ‚€' x = F .Fβ‚€' x
  Objects-universal F .vert .F₁' f' .hom' = F .F₁' f'
  Objects-universal F .vert .F₁' f' .cartesian =
    F .F-cartesian f' (R-right.cartesian f')
  Objects-universal F .vert .F-id' =
    Cartesian-morphism-pathp E (F .F-id')
  Objects-universal F .vert .F-∘' =
    Cartesian-morphism-pathp E (F .F-∘')
  Objects-universal F .F-cartesian f' cart =
    Objects-cartesian _

    : (F : Vertical-fibred-functor R E)
    β†’ F ≑ Objects-forget Vf∘ Objects-universal F
  Objects-factors F =
    Vertical-fibred-functor-path (Ξ» _ β†’ refl) (Ξ» _ β†’ refl)