Indexed 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 Homotopy 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 “Coproduct” you are thinking of is the domain $E$ of the bundle in the slice category.

$$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$)

Agda Example

The distinction is explicit in Agda syntax:

-- The Family (The Functor)
-- Maps an index to a Type.
Fam : I → Set
Fam i = ...
 
-- The Coproduct (The Total Space)
-- The actual object wrapping all elements.
Total : Set
Total = Σ I Fam

Would you like me to explain how this relates to the Grothendieck construction for converting functors into fibrations?