Family Fibration

Definition

A family fibration is the Grothendieck Fibration over Set obtained as the Grothendieck construction of the pseudofunctor
$P:{\mathbf{Set}}^{op}\Rightarrow \mathbf{Cat},P(I):={\mathbf{Set}}^I,$
with reindexing given by precomposition. Concretely, its total category has:

• Objects: pairs $(I,X)$ with a set-indexed family $X:I\to \mathbf{Set}$.
• Morphisms: a morphism $(u,\phi ):(I^{\prime },X^{\prime })\to (I,X)$ consists of a function $u:I^{\prime }\to I$ and a family of functions ${\phi }_{i^{\prime }}:X_{i^{\prime }}^{\prime }\to X_{u(i^{\prime })}$, equivalently a natural transformation $X^{\prime }\Rightarrow u^{\ast }X$.

The projection
$p:\mathcal{E}\Rightarrow \mathcal{B},\mathcal{E}=\mathrm{Fam}(\mathbf{Set}),\mathcal{B}=\mathbf{Set},$
$p(I,X)=I,p(u,\phi )=u,$
is a Grothendieck fibration; cartesian liftings are given by reindexing families along functions.

Fibres and morphisms

• Fibre over $I\in \mathcal{B}$: the functor category ${\mathbf{Set}}^I$.
• Vertical morphisms (over ${\mathrm{id}}_I$): pointwise functions $({\phi }_i:X_i\to X_i^{\prime }{)}_{i\in I}$.

Reindexing

For $u:I^{\prime }\to I$ and $X:I\to \mathbf{Set}$, reindexing is strict precomposition
$u^{\ast }X:=X\circ u:I^{\prime }\to \mathbf{Set},(u^{\ast }X{)}_{i^{\prime }}=X_{u(i^{\prime })}.$
On morphisms, $u^{\ast }$ acts pointwise. This yields a strictly functorial action:
$({\mathrm{id}}_I{)}^{\ast }={\mathrm{Id}}_{{\mathbf{Set}}^I},(u\circ v{)}^{\ast }=v^{\ast }\circ u^{\ast }.$

Cloven and split structure

With reindexing given by strict precomposition, the cleavage choosing the canonical cartesian liftings makes
$p:\mathcal{E}\Rightarrow \mathcal{B}$
a Split Fibration (hence in particular a Cloven Fibration).

Relation to set-indexed families and comprehension

• As objects, $(I,X)$ is exactly a Set-Indexed Family over $I$.
• The associated total space and projection
  ${\pi }_1:{\sum }_{i\in I}{X}_i\to I$
  are the comprehension of the family $X$. The family fibration organises all such projections uniformly over varying bases and families.
• In logical terms, predicates over $I$ are families $X:I\to \mathbf{Set}$; reindexing $u^{\ast }$ is substitution along $u$. Left/right adjoints to $u^{\ast }$ (when they exist) model dependent sums/products.

Examples

• Constant family: for a fixed set $F$, the object $(I,\lambda i.F)$ has total space $I\times F$ and projection $I\times F\to I$.
• Pullback of families: given $u:I^{\prime }\to I$, the cartesian lift of $u$ at $(I,X)$ is $(u,\mathrm{id}):(I^{\prime },u^{\ast }X)\to (I,X)$.
• Slices via comprehension: a function ${\pi }_1:{\sum }_{i\in I}{X}_i\to I$ recovers $X$ by fibres $X_i={\pi }_1^{-1}(i)$.

Related Concepts

Fibration
Grothendieck Fibration
Cloven Fibration
Split Fibration
Set-Indexed Family
Simple Fibration
Codomain Fibration
Opfibration
Dependent Sum
Dependent Product

References

jacobs1999-categorical-logic