module Cat.Displayed.Instances.Objects
  {o  o′ ℓ′} {B : Precategory o }
  (E : Displayed B o′ ℓ′)

The Fibration of Objects🔗

Let EB\mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B} 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 E\mathcal{E}, 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 E\mathcal{E}.

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 E\mathcal{E}, 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 EE 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 R\mathcal{R} and a fibred functor F:REF : \mathcal{R} \to \mathcal{E}: to complete the analogy, we show FF factors through E\mathcal{E}’s 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)