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 displayed over then a functor defines a (contravariant) βchange-of-baseβ action, resulting in a category displayed over

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 must have a space of objects; But our category has a space of objects. Fortunately, gives us a map which allows us to convert our to The same goes for indexing the displayed

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 is indeed a displayed category is a bit trickier than it might seem β we must adjust the identity and composites in by the paths witnessing functoriality of 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 is a cartesian fibration, then the base change of along is also cartesian. To prove this, observe that the object and hom spaces of Change-of-base contain the same data as just restricted to objects and morphisms in the image of This means that we still have cartesian lifts of all morphisms in we just have to perform the lifting of 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' β