Domain Opfibration

The domain opfibration of a category ℬ ℬ \mathcal{B} with Pushouts is the Cocartesian Fibration obtained from the functor Dom : ℬ → → ℬ : Dom → superscript ℬ → ℬ \mathrm{Dom}:\mathcal{B}^{\to}\to\mathcal{B} . In Displayed terms, this means that an object over I : ℬ : 𝐼 ℬ I:\mathcal{B} is a Coslice ( X , I → X ) → 𝑋 𝐼 𝑋 (X,I\to X) , and the morphisms over I → J → 𝐼 𝐽 I\to J are the obvious commuting squares.

This is the dual to the Codomain Fibration, and is fact always a Cartesian Fibration; base change involves diagrams of the form

∙∙{\bullet}I𝐼{I}J𝐽{J}u𝑢\scriptstyle{u}f𝑓\scriptstyle{f}

which can easily be pulled back by just composing.