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 XX to families over YY 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