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 private module Fib = Cat.Displayed.Fibre.Reasoning E
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.uniquep f x _ _ _ _ $ idr' _ β[] symP (idl' _) base-change .F-β {x} {y} {z} f' g' = sym $ has-lift.uniquep f z _ _ _ _ $ Fib.pulllf (has-lift.commutesp f z id-comm _) β[] pullr[] _ (has-lift.commutesp f y id-comm _) β[] pulll[] _ Fib.to-fibre
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.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)