module Cat.Displayed.Cartesian.Indexing {o ℓ o′ ℓ′} {B : Precategory o ℓ} (E : Displayed B o′ ℓ′) (cartesian : Cartesian-fibration E) where
open Cartesian-fibration cartesian open Cat.Displayed.Reasoning E open Cat.Reasoning B open Cartesian-lift open Displayed E open is-cartesian open Functor
Reindexing for Cartesian fibrations🔗
A cartesian fibration can be thought of as a displayed category whose fibre categories depend (pseudo)functorially on the object from the base category. A canonical example is the canonical self-indexing: If is a category with pullbacks, then each gives rise to a functor , the change of base along .
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
base-change .F-id {x} = sym $ has-lift.uniquev _ _ _ $ to-pathp $ idr[] ∙ (sym $ cancel _ _ (idl′ _)) base-change .F-∘ {x} {y} {z} f′ g′ = sym $ has-lift.uniquev _ _ _ $ to-pathp $ smashr _ _ ·· revive₁ (pulll[] (idr f) (has-lift.commutesv _ _ _)) ·· smashl _ _ ·· revive₁ (pullr[] (idr f) (has-lift.commutesv _ _ _)) ·· smashr _ _ ·· assoc[] ·· sym (smashl _ _)
Moreover, this assignment is itself functorial in : 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.uniquev₂ id x Fa.id _ (cast[] $ idr′ _) $ to-pathp (smashr _ _ ∙ cancel _ _ (cancell[] _ (has-lift.commutesv _ _ _))) mi .natural x y f = ap hom[] $ sym $ has-lift.commutes _ _ _ _ ·· hom[]-∙ _ _ ·· liberate _
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.uniquev₂ g _ _ _ (to-pathp $ smashr _ _ ·· revive₁ (pulll[] _ (has-lift.commutesv g _ _)) ·· has-lift.uniquep₂ f _ refl refl refl _ _ (pulll-indexr _ (has-lift.commutes f _ _ _) ∙ cancel _ _ (has-lift.commutesv (f ∘ g) _ _)) refl) (idr′ _) mi .inv∘eta x = has-lift.uniquev₂ (f ∘ g) _ _ _ (to-pathp $ smashr _ _ ·· revive₁ (pulll[] _ (has-lift.commutesv (f ∘ g) _ _)) ·· revive₁ (pullr[] _ (has-lift.commutesv g _ _)) ∙ cancel _ _ (has-lift.commutes f _ _ _)) (idr′ _) mi .natural x y f′ = ap hom[] $ cartesian→weak-monic E (has-lift.cartesian g _) _ _ $ from-pathp⁻ (pulll[] _ (has-lift.commutes g _ _ _)) ·· smashl _ _ ·· smashl _ _ ·· revive₁ (pullr[] _ (has-lift.commutesv g _ _ )) ·· (cartesian→weak-monic E (has-lift.cartesian f _) _ _ $ whisker-r _ ·· revive₁ (pulll[] _ (has-lift.commutesv f _ _)) ·· smashl _ _ ·· revive₁ (pullr[] _ (has-lift.commutes f _ _ _)) ·· duplicate _ (ap (f ∘_) (intror (idl id))) _ ·· revive₁ (symP (has-lift.commutesv (f ∘ g) _ _)) ·· revive₁ (pushl[] _ (symP $ has-lift.commutes f _ _ _)) ·· unwhisker-r _ (ap (g ∘_) (sym $ idl id)) ·· ap (has-lift.lifting f _ ∘′_) (expandl _ _ ∙ reindex _ _)) ∙ cancel (sym $ assoc _ _ _) _ (pushl[] _ (symP $ has-lift.commutes g _ _ _))