nLab family of sets



In set theory

A family of sets consists of an index set II and, for each element kk of II, a set S kS_k.

Given II, a set FF and a function p:FIp\colon F \to I, we get a family of sets by defining S kS_k to be the preimage p *(k)p^*(k).

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

kS k={(k,x)|kI,xS k} \biguplus_k S_k = \{ (k,x) | k \in I, x \in S_k \}

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

(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.)

In category theory

A family of sets consists of an discrete groupoid II called the index set, and a functor F:ISetF:I \to Set, where Set is the large category of sets.

In dependent type theory

A family of sets consists of a type II called the index type, and a type family S(x)S(x) indexed by elements x:Ix:I, such that every dependent type S(x)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)(I, S) which satisfies the familial axiom K.

Inconsistency of the universal family of sets

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

See also

Last revised on November 20, 2022 at 04:50:30. See the history of this page for a list of all contributions to it.