module Cat.Displayed.Cartesian.Indexing
  {o ℓ o' ℓ'} {B : Precategory o ℓ}
  (E : Displayed B o' ℓ')
  (cartesian : Cartesian-fibration E)
  where

Reindexing for cartesian fibrations🔗

A cartesian fibration can be thought of as a displayed category $\mathcal{E}$ whose fibre categories $\mathcal{E}^*(b)$ depend (pseudo)functorially on the object $b : \mathcal{B}$ from the base category. A canonical example is the canonical self-indexing: If $\mathcal{C}$ is a category with pullbacks, then each $b \xrightarrow{f} a : \mathcal{C}$ gives rise to a functor $\mathcal{C}/a \to \mathcal{C}/b$ , the change of base along $f$ .

module _ {𝒶 𝒷} (f : Hom 𝒶 𝒷) where
  base-change : Functor (Fibre E 𝒷) (Fibre E 𝒶)
  base-change .F₀ ob = has-lift f ob .x'
  base-change .F₁ {x} {y} vert = rebase f vert

Moreover, this assignment is itself functorial in $f$ : Along the identity morphism, it’s the same thing as not changing bases at all.

module _ {𝒶} where
  private
    module FC = Cat.Reasoning (Cat[ Fibre E 𝒶 , Fibre E 𝒶 ])
    module Fa = Cat.Reasoning (Fibre E 𝒶)

  base-change-id : base-change id FC.≅ Id

I’ll warn you in advance that this proof is not for the faint of heart.

  base-change-id = to-natural-iso mi where
    open make-natural-iso
    mi : make-natural-iso (base-change id) Id
    mi .eta x = has-lift.lifting id x
    mi .inv x = has-lift.universalv id x id'
    mi .eta∘inv x = cancel _ _ (has-lift.commutesv _ _ _)
    mi .inv∘eta x = sym $
      has-lift.uniquep₂ id x _ _ _ _ _
        (idr' _)
        (Fib.cancellf (has-lift.commutesv _ _ _))
    mi .natural x y f =
      sym $ from-pathp $ cast[] $
        has-lift.commutesp id y id-comm _
        ∙[] Fib.to-fibre

And similarly, composing changes of base is the same thing as changing base along a composite.

module _ {𝒶} {𝒷} {𝒸} (f : Hom 𝒷 𝒸) (g : Hom 𝒶 𝒷) where
  private
    module FC = Cat.Reasoning (Cat[ Fibre E 𝒸 , Fibre E 𝒶 ])
    module Fa = Cat.Reasoning (Fibre E 𝒶)

  base-change-comp : base-change (f ∘ g) FC.≅ (base-change g F∘ base-change f)

This proof is a truly nightmarish application of universal properties and I recommend that nobody look at it, ever.

  base-change-comp = to-natural-iso mi where
    open make-natural-iso
    mi : make-natural-iso (base-change (f ∘ g)) (base-change g F∘ base-change f)
    mi .eta x =
      has-lift.universalv g _ $ has-lift.universal f x g (has-lift.lifting (f ∘ g) x)
    mi .inv x =
      has-lift.universalv (f ∘ g) x (has-lift.lifting f _ ∘' has-lift.lifting g _)
    mi .eta∘inv x =
      has-lift.uniquep₂ _ _ _ _ _ _ _
        (Fib.pulllf (has-lift.commutesv g _ _)
         ∙[] has-lift.uniquep₂ _ _ _ (idr _) refl _ _
           (pulll[] _ (has-lift.commutes _ _ _ _)
            ∙[] has-lift.commutesv _ _ _)
           refl)
        (idr' _)
    mi .inv∘eta x =
      has-lift.uniquep₂ _ _ _ _ _ _ _
        (Fib.pulllf (has-lift.commutesv _ _ _)
         ∙[] pullr[] _ (has-lift.commutesv _ _ _)
         ∙[] has-lift.commutes _ _ _ _)
        (idr' _)
    mi .natural x y f' =
      ap hom[] $ cartesian→weak-monic E (has-lift.cartesian g _) _ _ $ cast[] $
        pulll[] _ (has-lift.commutesp g _ id-comm _)
        ∙[] pullr[] _ (has-lift.commutesv g _ _)
        ∙[] has-lift.uniquep₂ _ _ _ id-comm-sym _ _ _
          (pulll[] _ (has-lift.commutesp _ _ id-comm _)
           ∙[] pullr[] _ (has-lift.commutes _ _ _ _))
          (pulll[] _ (has-lift.commutes _ _ _ _)
           ∙[] has-lift.commutesp _ _ id-comm _)
        ∙[] pushl[] _ (symP (has-lift.commutesv g _ _))