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 .
The reason for this contravariance is the following: A category displayed over must have a -indexed space of objects; But our category has a -indexed space of objects. Fortunately, gives us a map which allows us to convert our -indices to -indices. The same goes for indexing the displayed -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 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β² β