module Cat.Displayed.Instances.Pullback {o β o' β' o'' β''} {X : Precategory o β} {B : Precategory o' β'} (F : Functor X B) (E : Displayed B o'' β'') where

# Pullback of a displayed categoryπ

If we have a category $E$ displayed over $B,$ then a functor $F:XβB$ defines a (contravariant) βchange-of-baseβ action, resulting in a category $F_{β}(E)$ displayed over $X.$

private module X = Precategory X module B = Precategory B module E = Displayed E open Functor F open Displayed open Dr E

The reason for this contravariance is the following: A category displayed over $X$ must have a $X-indexed$ space of objects; But our category $E$ has a $B-indexed$ space of objects. Fortunately, $F$ gives us a map $xβ¦F_{0}(x)$ which allows us to convert our $X-indices$ to $B-indices.$ The same goes for indexing the displayed $Hom-sets.$

Change-of-base : Displayed X o'' β'' Change-of-base .Ob[_] x = E.Ob[ Fβ x ] Change-of-base .Hom[_] f x y = E.Hom[ Fβ f ] x y Change-of-base .Hom[_]-set f = E.Hom[ Fβ f ]-set Change-of-base .id' = hom[ sym F-id ] E.id' Change-of-base ._β'_ f' g' = hom[ sym (F-β _ _) ] (f' E.β' g')

Proving that the pullback $F_{β}(E)$ is indeed a displayed category is a bit trickier than it might seem β we must adjust the identity and composites in $E$ by the paths witnessing functoriality of $F,$ and this really throws a spanner in the works β but the handy displayed category reasoning combinators are here to help.

Change-of-base .idr' {f = f} f' = to-pathp $ hom[] (hom[ F-β _ _ ]β» (f' E.β' hom[ F-id ]β» _)) β‘β¨ hom[]β©β¨ smashr _ _ β©β‘ hom[] (hom[] (f' E.β' E.id')) β‘β¨ Ds.disp! E β©β‘ f' β Change-of-base .idl' f' = to-pathp $ hom[] (hom[ F-β _ _ ]β» (hom[ F-id ]β» _ E.β' f')) β‘β¨ hom[]β©β¨ smashl _ _ β©β‘ hom[] (hom[] (E.id' E.β' f')) β‘β¨ Ds.disp! E β©β‘ f' β Change-of-base .assoc' f' g' h' = to-pathp $ hom[ ap Fβ _ ] (hom[ F-β _ _ ]β» (f' E.β' hom[ F-β _ _ ]β» (g' E.β' h'))) β‘β¨ hom[]β©β¨ smashr _ _ β©β‘ hom[] (hom[] (f' E.β' g' E.β' h')) β‘β¨ Ds.disp! E β©β‘ hom[ sym (F-β _ _) ] (hom[ sym (F-β _ _) ] (f' E.β' g') E.β' h') β

## As a fibrationπ

If
$E$
is a cartesian
fibration, then the base change of
$E$
along
$F$
is also cartesian. To prove this, observe that the object and hom spaces
of `Change-of-base`

contain the same
data as
$E,$
just restricted to objects and morphisms in the image of
$F.$
This means that we still have cartesian lifts of all morphisms in
$X:$
we just have to perform the lifting of
$Ff.$

Change-of-base-fibration : Cartesian-fibration E β Cartesian-fibration Change-of-base Change-of-base-fibration fib .Cartesian-fibration.has-lift f FY' = cart-lift where open Cartesian-lift (Cartesian-fibration.has-lift fib (Fβ f) FY') cart-lift : Cartesian-lift Change-of-base f FY' cart-lift .Cartesian-lift.x' = x' cart-lift .Cartesian-lift.lifting = lifting cart-lift .Cartesian-lift.cartesian .is-cartesian.universal m h' = universal (F .Functor.Fβ m) (hom[ F-β f m ] h') cart-lift .Cartesian-lift.cartesian .is-cartesian.commutes m h' = hom[ F-β f m ]β» (lifting E.β' universal (Fβ m) (hom[ F-β f m ] h')) β‘β¨ ap hom[ F-β f m ]β» (commutes _ _) β©β‘ hom[ F-β f m ]β» (hom[ F-β f m ] h') β‘β¨ Ds.disp! E β©β‘ h' β cart-lift .Cartesian-lift.cartesian .is-cartesian.unique {m = m} {h' = h'} m' p = unique m' $ lifting E.β' m' β‘β¨ Ds.disp! E β©β‘ hom[ F-β f m ] (hom[ F-β f m ]β» (lifting E.β' m')) β‘β¨ ap hom[ F-β f m ] p β©β‘ hom[ F-β f m ] h' β