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 $X$ to families over $Y$ 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