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-fibred-functor
open Vertical-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-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

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