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

open Cat.Reasoning B open Displayed E open Cartesian-morphism open Vertical-fibred-functor open Vertical-functor

# The fibration of objectsπ

Let
$EB$
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,$
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 .Displayed.id' = 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.$

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,$ 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.

Objects-cartesian : β {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 $E$ 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 .Right-fibration.is-fibration = 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$ and a fibred functor $F:RβE:$ to complete the analogy, we show $F$ factors through $Eβs$ fibration of objects.

module _ {or βr} {R : Displayed B or βr} (R-right : Right-fibration R) where private open Vertical-fibred-functor module R-right = Right-fibration R-right

Objects-universal : (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 _ Objects-factors : (F : Vertical-fibred-functor R E) β F β‘ Objects-forget Vfβ Objects-universal F Objects-factors F = Vertical-fibred-functor-path (Ξ» _ β refl) (Ξ» _ β refl)