open import Cat.Displayed.Cocartesian open import Cat.Instances.Functor open import Cat.Displayed.Fibre open import Cat.Displayed.Base open import Cat.Prelude import Cat.Displayed.Reasoning import Cat.Reasoning module Cat.Displayed.Cocartesian.Indexing {o β oβ² ββ²} {β¬ : Precategory o β} (β° : Displayed β¬ oβ² ββ²) (opfibration : Cocartesian-fibration β°) where
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.
[reindex along morphisms in the base] Cat.Displayed.Cartesian.Indexing.html
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 the 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 = has-lift.yβ² f ob cobase-change f .Fβ vert = rebase f vert