open import Cat.Displayed.Cartesian.Right
open import Cat.Displayed.Cartesian
open import Cat.Displayed.Functor
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning
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-functor
open is-fibred-functor

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

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

Objects-forget-is-fibred : is-fibred-functor Objects-forget
Objects-forget-is-fibred .F-cartesian {f' = f'} _ = f' .cartesian
private module Objects = Displayed Objects

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.

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 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 f y' = f-lift where
  open Cartesian-fibration E fib

  f-lift : Cartesian-lift Objects f y'
  f-lift .Cartesian-lift.x' = f ^* y'
  f-lift .Cartesian-lift.lifting .hom' = Ο€* f y'
  f-lift .Cartesian-lift.lifting .cartesian = Ο€*.cartesian
  f-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 and a fibred functor to complete the analogy, we show factors through fibration of objects.

module _
  {or β„“r} {R : Displayed B or β„“r}
  (R-right : Right-fibration R)
  where
  private
    open Vertical-functor
    module R-right = Right-fibration R-right
  Objects-universal
    : (F : Vertical-functor R E)
    β†’ is-fibred-functor F
    β†’ Vertical-functor R Objects
  Objects-universal F F-fib .Fβ‚€' x = F .Fβ‚€' x
  Objects-universal F F-fib .F₁' f' .hom' = F .F₁' f'
  Objects-universal F F-fib .F₁' f' .cartesian = F-fib .F-cartesian (R-right.cartesian f')
  Objects-universal F F-fib .F-id' =
    Cartesian-morphism-pathp E (F .F-id')
  Objects-universal F F-fib .F-∘' =
    Cartesian-morphism-pathp E (F .F-∘')

  Objects-universal-fibred
    : (F : Vertical-functor R E)
    β†’ (F-fib : is-fibred-functor F)
    β†’ is-fibred-functor (Objects-universal F F-fib)
  Objects-universal-fibred F F-fib .F-cartesian cart = Objects-cartesian _

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