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 _ _))

In order to assemble this into a pseudofunctor out of $\mathcal{B}^{\mathrm{op}}$ (seen as a locally discrete bicategory) into $\mathfrak{Cat}$ , we start by bundling up all the base changes into a functor between $\mathbf{Hom}$ categories. We also prove a lemma that will be useful later, relating base changes along equal morphisms.

base-changes : ∀ {a b}
  → Functor (Locally-discrete (B ^op) .Prebicategory.Hom a b)
            Cat[ Fibre E a , Fibre E b ]
base-changes = Disc-adjunct base-change

base-change-coherence
  : ∀ {a b} {b' : Ob[ b ]} {f g : Hom a b} (p : f ≡ g)
  → has-lift.lifting g b' ∘' base-changes .F₁ p .η b'
  ≡[ idr _ ∙ sym p ] has-lift.lifting f b'
base-change-coherence {b' = b'} {f} = J
  (λ g p → has-lift.lifting g b' ∘' base-changes .F₁ p .η b'
         ≡[ idr _ ∙ sym p ] has-lift.lifting f b')
  (elimr' refl Regularity.reduce!)

We have enough data to start defining our pseudofunctor:

Fibres : Pseudofunctor (Locally-discrete (B ^op)) (Cat o' ℓ')
Fibres .lax .P₀ = Fibre E
Fibres .lax .P₁ = base-changes
Fibres .lax .compositor = Disc-natural₂
  λ (f , g) → base-change-comp g f .Mor.from
Fibres .lax .unitor = base-change-id .Mor.from
Fibres .unitor-inv = FC.iso→invertible (base-change-id FC.Iso⁻¹)
Fibres .compositor-inv f g =
  FC.iso→invertible (base-change-comp g f FC.Iso⁻¹)

It remains to verify that this data is coherent, which is so tedious that it serves as a decent self-contained motivation for displayed categories.

You’ve been warned.

We start with the left-unit. In the diagram below, we have to show that the composite vertical morphism over $b$ is equal to the identity over $b$ . By the uniqueness property of cartesian lifts, it suffices to show that the composites with the lift of $f$ are equal, which is witnessed by the commutativity of the whole diagram.

The bottom triangle is our base-change-coherence lemma, the middle square is by definition of the compositor and the top triangle is by definition of the unitor.

Fibres .lax .left-unit f = Nat-path λ a' →
  has-lift.uniquep₂ f a' _ refl refl _ _
    (Fib.pulllf (base-change-coherence (idr f))
    ∙[] Fib.pulllf (has-lift.commutesv (f ∘ id) a' _)
    ∙[] (refl⟩∘'⟨ Fib.eliml (base-change id .F-id))
    ∙[] pullr[] _ (has-lift.commutesv id _ id'))
    refl

For the right-unit, we proceed similarly. The diagram below shows that the composite on the left, composed with the lift of $f$ , is equal to the lift of $f$ .

The bottom triangle is base-change-coherence, the middle square is by definition of the compositor, the outer triangle is by definition of the unitor, and the top square is by definition of rebase (the action of $f^*$ on morphisms).

Fibres .lax .right-unit f = Nat-path λ a' →
  has-lift.uniquep₂ f a' _ refl _ _ _
    (Fib.pulllf (base-change-coherence (idl f))
    ∙[] Fib.pulllf (has-lift.commutesv (id ∘ f) a' _)
    ∙[] (refl⟩∘'⟨ Fib.idr _)
    ∙[] extendr[] id-comm (has-lift.commutesp f _ _ _)
    ∙[] (has-lift.commutesv id _ id' ⟩∘'⟨refl))
    (idr' _ ∙[] symP (idl' _))

Last but definitely not least, the hexagon witnessing the coherence of associativity follows again by uniqueness of cartesian lifts, by the commutativity of the following diagram.

Fibres .lax .hexagon f g h = Nat-path λ a' →
  has-lift.uniquep₂ ((h ∘ g) ∘ f) a' _ refl _ _ _
    (Fib.pulllf (base-change-coherence (assoc h g f))
    ∙[] Fib.pulllf (has-lift.commutesv (h ∘ (g ∘ f)) a' _)
    ∙[] (refl⟩∘'⟨ Fib.eliml (base-change (g ∘ f) .F-id))
    ∙[] extendr[] _ (has-lift.commutesv (g ∘ f) _ _))
    (Fib.pulllf (has-lift.commutesv ((h ∘ g) ∘ f) a' _)
    ∙[] (refl⟩∘'⟨ Fib.idr _) ∙[] (refl⟩∘'⟨ Fib.idr _)
    ∙[] extendr[] id-comm (has-lift.commutesp f _ _ _)
    ∙[] (has-lift.commutesv (h ∘ g) a' _ ⟩∘'⟨refl))