{o β„“ o' β„“' o'' β„“''}
    {X : Precategory o β„“} {B : Precategory o' β„“'}
    (F : Functor X B)
    (E : Displayed B o'' β„“'')

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 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 ]'
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.∘''))                    β‰‘βŸ¨ Ds.disp! E βŸ©β‰‘
  f'                                               ∎

Change-of-base .idl' f' = to-pathp $
  hom[] (hom[ F-∘ _ _ ]⁻ (hom[ F-id ]⁻ _ E.∘' f')) β‰‘βŸ¨ hom[]⟩⟨ smashl _ _ βŸ©β‰‘
  hom[] (hom[] (' 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
    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' ∎