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 E\mathcal{E} whose fibre categories Eβˆ—(b)\mathcal{E}^*(b) depend (pseudo)functorially on the object b:Bb : \mathcal{B} from the base category. A canonical example is the canonical self-indexing: If C\mathcal{C} is a category with pullbacks, then each bβ†’fa:Cb \xrightarrow{f} a : \mathcal{C} gives rise to a functor C/aβ†’C/b\mathcal{C}/a \to \mathcal{C}/b, the change of base along ff.

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 ff: 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 _ _))
-- Optimized natural iso, avoids a bunch of junk from composition.
opaque
  base-change-square
    : βˆ€ {Ξ“ Ξ” Θ Ξ¨ : Ob}
    β†’ {Οƒ : Hom Ξ“ Ξ”} {Ξ΄ : Hom Ξ“ Θ} {Ξ³ : Hom Ξ” Ξ¨} {Ο„ : Hom Θ Ξ¨}
    β†’ Ξ³ ∘ Οƒ ≑ Ο„ ∘ Ξ΄
    β†’ βˆ€ x' β†’ Hom[ id ]
      (base-change Οƒ .Fβ‚€ (base-change Ξ³ .Fβ‚€ x'))
      (base-change Ξ΄ .Fβ‚€ (base-change Ο„ .Fβ‚€ x'))
  base-change-square {Οƒ = Οƒ} {Ξ΄ = Ξ΄} {Ξ³ = Ξ³} {Ο„ = Ο„} p x' =
    has-lift.universalv Ξ΄ _ $
    has-lift.universal' Ο„ _ (sym p) $
    has-lift.lifting Ξ³ x' ∘' has-lift.lifting Οƒ _

  base-change-square-lifting
    : βˆ€ {Ξ“ Ξ” Θ Ξ¨ : Ob}
    β†’ {Οƒ : Hom Ξ“ Ξ”} {Ξ΄ : Hom Ξ“ Θ} {Ξ³ : Hom Ξ” Ξ¨} {Ο„ : Hom Θ Ξ¨}
    β†’ (p : Ξ³ ∘ Οƒ ≑ Ο„ ∘ Ξ΄) (x' : Ob[ Ξ¨ ])
    β†’ has-lift.lifting Ο„ x' ∘' has-lift.lifting Ξ΄ (base-change Ο„ .Fβ‚€ x') ∘' base-change-square p x'
    ≑[ ap (Ο„ ∘_) (idr _) βˆ™ sym p ] has-lift.lifting Ξ³ x' ∘' has-lift.lifting Οƒ _
  base-change-square-lifting {Οƒ = Οƒ} {Ξ΄ = Ξ΄} {Ξ³ = Ξ³} {Ο„ = Ο„} p x' =
    cast[] $
    apd (Ξ» _ β†’ has-lift.lifting Ο„ x' ∘'_) (has-lift.commutesv _ _ _)
    βˆ™[] has-lift.commutesp Ο„ x' (sym p) _

  base-change-square-natural
    : βˆ€ {Ξ“ Ξ” Θ Ξ¨ : Ob}
    β†’ {Οƒ : Hom Ξ“ Ξ”} {Ξ΄ : Hom Ξ“ Θ} {Ξ³ : Hom Ξ” Ξ¨} {Ο„ : Hom Θ Ξ¨}
    β†’ (p : Ξ³ ∘ Οƒ ≑ Ο„ ∘ Ξ΄)
    β†’ βˆ€ {x' y'} (f' : Hom[ id ] x' y')
    β†’ base-change-square p y' ∘' base-change Οƒ .F₁ (base-change Ξ³ .F₁ f')
    ≑ base-change Ξ΄ .F₁ (base-change Ο„ .F₁ f') ∘' base-change-square p x'
  base-change-square-natural {Οƒ = Οƒ} {Ξ΄ = Ξ΄} {Ξ³ = Ξ³} {Ο„ = Ο„} p f' =
    has-lift.uniquepβ‚‚ Ξ΄ _ _ _ _ _ _
      (pulll[] _ (has-lift.commutesv Ξ΄ _ _)
       βˆ™[] has-lift.uniquepβ‚‚ Ο„ _ _ (idr _) _ _ _
         (pulll[] _ (has-lift.commutesp Ο„ _ (sym p) _)
          βˆ™[] pullr[] _ (has-lift.commutesp Οƒ _ id-comm _)
          βˆ™[] extendl[] _ (has-lift.commutesp Ξ³ _ id-comm _))
         (has-lift.commutesp Ο„ _ (sym p βˆ™ sym (idl _ )) _))
      (pulll[] _ (has-lift.commutesp Ξ΄ _ id-comm _)
       βˆ™[] pullr[] _ (has-lift.commutesv Ξ΄ _ _)
       βˆ™[] has-lift.uniquep Ο„ _ _ (idl _) (sym p βˆ™ sym (idl _)) _
         (pulll[] _ (has-lift.commutesp _ _ id-comm _ )
          βˆ™[] pullr[] _ (has-lift.commutesp _ _ (sym p) _)))

  base-change-square-inv
    : βˆ€ {Ξ“ Ξ” Θ Ξ¨ : Ob}
    β†’ {Οƒ : Hom Ξ“ Ξ”} {Ξ΄ : Hom Ξ“ Θ} {Ξ³ : Hom Ξ” Ξ¨} {Ο„ : Hom Θ Ξ¨}
    β†’ (p : Ξ³ ∘ Οƒ ≑ Ο„ ∘ Ξ΄)
    β†’ βˆ€ x' β†’ base-change-square p x' ∘' base-change-square (sym p) x' ≑[ idl _ ] id'
  base-change-square-inv {Οƒ = Οƒ} {Ξ΄ = Ξ΄} {Ξ³ = Ξ³} {Ο„ = Ο„} p x' =
    has-lift.uniquepβ‚‚ _ _ _ _ _ _ _
      (pulll[] _ (has-lift.commutesv Ξ΄ _ _)
       βˆ™[] has-lift.uniquepβ‚‚ Ο„ _ _ (idr _) refl _ _
         (pulll[] _ (has-lift.commutesp Ο„ _ (sym p) _)
          βˆ™[] pullr[] _ (has-lift.commutesv Οƒ _ _)
          βˆ™[] has-lift.commutesp Ξ³ _ p _)
         refl)
      (idr' _)

base-change-square-ni
  : βˆ€ {Ξ“ Ξ” Θ Ξ¨ : Ob}
  β†’ {Οƒ : Hom Ξ“ Ξ”} {Ξ΄ : Hom Ξ“ Θ} {Ξ³ : Hom Ξ” Ξ¨} {Ο„ : Hom Θ Ξ¨}
  β†’ Ξ³ ∘ Οƒ ≑ Ο„ ∘ Ξ΄
  β†’ (base-change Οƒ F∘ base-change Ξ³) ≅ⁿ (base-change Ξ΄ F∘ base-change Ο„)
base-change-square-ni {Οƒ = Οƒ} {Ξ΄ = Ξ΄} {Ξ³ = Ξ³} {Ο„ = Ο„} p =
  to-natural-iso ni where

  open make-natural-iso
  ni : make-natural-iso _ _
  ni .eta = base-change-square p
  ni .inv = base-change-square (sym p)
  ni .eta∘inv x = from-pathp $ base-change-square-inv p x
  ni .inv∘eta x = from-pathp $ base-change-square-inv (sym p) x
  ni .natural x y f = sym $ Fib.over-fibre (base-change-square-natural p f)