Set-Indexed Family

Definition

A set-indexed family over a base set $B$ is a function $E:B\to \mathbf{Set}$, written as a collection of fibres $(E_b{)}_{b\in B}$. Equivalently, it is a function of sets $p:\tilde{E}\to B$ whose fibre over $b\in B$ is $E_b=p^{-1}(b)$. The two presentations are related by the comprehension/total space construction $\tilde{E}\cong {\sum }_{b\in B}{E}_b=\{(b,x)\mid b\in B,x\in E_b\},{\pi }_1:{\sum }_{b\in B}{E}_b\to B.$

Notation

• Family form: $(E_b{)}_{b\in B}$ or $E:B\to \mathbf{Set}$.
• Total space and projection: ${\pi }_1:{\sum }_{b\in B}{E}_b\to B$, with fibre $({\pi }_1{)}^{-1}(b)\cong E_b$.
• In type-theoretic notation, a dependent type $E:B\to \mathcal{U}$ corresponds to the projection ${\pi }_1:{\sum }_{b:B}E(b)\to B$.

Reindexing

Given $f:B^{\prime }\to B$ and a family $E:B\to \mathbf{Set}$, the pullback (reindexed) family $f^{\ast }E:B^{\prime }\to \mathbf{Set}$ is defined by $(f^{\ast }E{)}_{b^{\prime }}:=E_{f(b^{\prime })}$. This operation is strictly functorial: ${\mathrm{id}}^{\ast }=\mathrm{Id}$ and $(g\circ f{)}^{\ast }=f^{\ast }\circ g^{\ast }$.

Morphisms of families

• Over the same base $B$: a morphism $(E_b{)}_{b\in B}\to (E_b^{\prime }{)}_{b\in B}$ is a family of functions $({\phi }_b:E_b\to E_b^{\prime }{)}_{b\in B}$.
• Over different bases: a morphism over $f:B\to B^{\prime }$ consists of functions ${\phi }_b:E_b\to E_{f(b)}^{\prime }$, natural in $b$.

Examples

• Constant family: for $F$ a set, $E_b=F$ for all $b\in B$; total space $B\times F\to B$.
• Singleton family: $E_b=1$ for all $b$; total space $B\to B$ is the identity.
• Fibres of a function: given $p:\tilde{E}\to B$, define $E_b=p^{-1}(b)$; conversely, $(E_b{)}_{b\in B}$ determines ${\pi }_1:{\sum }_{b\in B}{E}_b\to B$.

Related Concepts

• Fibration
• Grothendieck Fibration
• Family Fibration
• Codomain Fibration
• Dependent Sum
• Dependent Product