A family of sets consists of an index set$I$ and, for each element$k$ of $I$, a set$S_k$.

Given $I$, a set$F$ and a function$p\colon F \to I$, we get a family of sets by defining $S_k$ to be the preimage$p^*(k)$.

Conversely, given a family of sets, let $F$ be the disjoint union

$\biguplus_k S_k = \{ (k,x) | k \in I, x \in S_k \}$

and let $f(k,x)$ be $k$.

(We should talk about ways to formalise this concept in various forms of set theory and when the latter construction above requires the axiom of collection.)

A family of sets consists of a type $I$ called the index type, and a type family$S(x)$ indexed by elements $x:I$, such that every dependent type $S(x)$ is an h-set by the typal axiom K definition or the typal uniqueness of identity proofs definition.

Equivalently, it is a type family $(I, S)$ which satisfies the familial axiom K.

Inconsistency of the universal family of sets

A universal family of sets is a set $U$ with a set $I$ and a function $E:U \to I$ such that for all sets $A$, there is a unique element $i_A \in I$ and a bijection$\delta_A:A \cong E^*(i_A)$ from $A$ to the fiber of $E$ at $i_A$. This is inconsistent in any set theory, due to the set-theoretic Girard's paradox.