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