module Cat.Displayed.Cocartesian.Indexing {o ℓ o' ℓ'} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o' ℓ') (opfibration : Cocartesian-fibration ℰ) where
open Precategory ℬ open Displayed ℰ open Cat.Displayed.Reasoning ℰ open Cocartesian-fibration ℰ opfibration open Functor
Opreindexing for cocartesian fibrations🔗
Opfibrations are dual to fibrations, so they inherit the ability to reindex along morphisms in the base. However, this reindexing is covariant for opfibrations, whereas it is contravariant for fibrations.
This difference in variance gives opfibrations a distinct character. Reindexing in fibrations can be thought of a sort of restriction map. This can be seen clearly with canonical self-indexing, where the reindexing functors are given by pullbacks. On the other hand, opreindexing can be thought of as an extension map. We can again use the the canonical self-indexing as our example: opreindexing is given by postcomposition, which extends families over to families over by adding in empty fibres.
cobase-change : ∀ {x y} (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y) cobase-change f .F₀ ob = f ^! ob cobase-change f .F₁ vert = rebase f vert
cobase-change f .F-id = sym $ ι!.uniquev _ $ to-pathp $ idl[] ∙ (sym $ cancel _ _ (idr' _)) cobase-change f .F-∘ f' g' = sym $ ι!.uniquev _ $ to-pathp $ smashl _ _ ∙∙ revive₁ (pullr[] _ (ι!.commutesv _)) ∙∙ smashr _ _ ∙∙ revive₁ (pulll[] _ (ι!.commutesv _)) ∙∙ smashl _ _ ∙∙ sym assoc[] ∙∙ sym (smashr _ _)