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

import Cat.Displayed.Reasoning as Dr
import Cat.Displayed.Solver as Ds

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 \to 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 \mapsto F_0(x)$ which allows us to convert our $X$-indices to $B$-indices. The same goes for indexing the displayed $\mathbf{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 $\mathcal{E}$ is a cartesian fibration, then the base change of $\mathcal{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 $\mathcal{E}$, just restricted to objects and morphisms in the image of $F$. This means that we still have cartesian lifts of all morphisms in $\mathcal{X}$: we just have to perform the lifting of $F f$. 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' β