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 EE displayed over BB, then a functor F:Xβ†’BF : X \to B defines a (contravariant) β€œchange-of-base” action, resulting in a category Fβˆ—(E)F^*(E) displayed over XX.

The reason for this contravariance is the following: A category displayed over XX must have a XX-indexed space of objects; But our category EE has a BB-indexed space of objects. Fortunately, FF gives us a map x↦F0(x)x \mapsto F_0(x) which allows us to convert our XX-indices to BB-indices. The same goes for indexing the displayed Hom\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)F^*(E) is indeed a displayed category is a bit trickier than it might seem β€” we must adjust the identity and composites in EE by the paths witnessing functoriality of FF, 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\mathcal{E} is a cartesian fibration, then the base change of E\mathcal{E} along FF is also cartesian. To prove this, observe that the object and hom spaces of Change-of-base contain the same data as E\mathcal{E}, just restricted to objects and morphisms in the image of FF. This means that we still have cartesian lifts of all morphisms in X\mathcal{X}: we just have to perform the lifting of FfF 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' ∎