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 $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

cobase-change f .F-id = sym $ has-lift.uniquev _ _ _ $ to-pathp $ idl[] β (sym $ cancel _ _ (idr' _)) cobase-change f .F-β f' g' = sym $ has-lift.uniquev _ _ _ $ to-pathp $ smashl _ _ Β·Β· reviveβ (pullr[] _ (has-lift.commutesv _ _ _)) Β·Β· smashr _ _ Β·Β· reviveβ (pulll[] _ (has-lift.commutesv _ _ _)) Β·Β· smashl _ _ Β·Β· sym assoc[] Β·Β· sym (smashr _ _)