typical contexts
A family of sets consists of an index set and, for each element of , a set .
Given , a set and a function , we get a family of sets by defining to be the preimage .
Conversely, given a family of sets, let be the disjoint union
and let be .
(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 an discrete groupoid called the index set, and a functor , where Set is the large category of sets.
A family of sets consists of a type called the index type, and a type family indexed by elements , such that every dependent type is an h-set by the typal axiom K definition or the typal uniqueness of identity proofs definition.
Equivalently, it is a type family which satisfies the familial axiom K.
A universal family of sets is a set with a set and a function such that for all sets , there is a unique element and a bijection from to the fiber of at . This is inconsistent in any set theory, due to the set-theoretic Girard's paradox.
Last revised on November 20, 2022 at 04:50:30. See the history of this page for a list of all contributions to it.