Type Family

Definition

A type family is a function from an index type to a universe:

$$B:I\to \mathcal{U}$$

This assigns a type $B(i)$ to every term $i:I$.

Remarks

In $\mathbf{Set}$ (and analogous topoi), there is an equivalence of categories:

$${\mathbf{Set}}^I\simeq \mathbf{Set}/I$$

• LHS (Functor view): The indexed family $B:I\to \mathbf{Set}$.
• RHS (Slice view): A Bundle $p:E\to I$.

The domain $E$ of the bundle in the slice category is isomorphic to the coproduct,

$$E\cong \sum _{i:I}B(i)\cong \coprod _{i\in I}B(i)$$

The indexed family corresponds to the fibers of the map $p:\coprod B(i)\to I$, not just the coproduct object itself. The coproduct alone forgets which element belongs to which index unless equipped with the projection to $I$.

Summary Table

Concept	Type Theory	Category Theory
Family	$B:I\to \mathcal{U}$	Functor $F:\mathcal{I}\to \mathcal{C}$ (discrete $\mathcal{I}$)
Total Space	$\Sigma (i:I).B(i)$	Coproduct ${\coprod }_{i\in I}F(i)$
Bundle Map	${\pi }_1:(\Sigma B)\to I$	Projection $p:(\coprod F)\to I$
Relationship	”Fibration” (Dependent Sum)	Grothendieck Construction ($\int F$)