homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
Just as a subobject classifier in a (1,1)-category classifies the monomorphisms or (-1)-truncated morphisms (and thus the subobjects) of the category, a discrete object classifier in a (2,1)-category should classify the faithful or 0-truncated morphisms (and thus the discrete objects) in the (2,1)-category, see at n-truncated morphisms – between groupoids.
In a (2,1)-category $C$ with terminal object $*$, interval object $I$, and finite (2,1)-pullbacks, a discrete object classifier is a morphism $inhabited: [I, Set] \rightarrow Set$ whose target is a nonterminal object $Set$ and whose source is the internal hom-object $[I, Set]$ such that for every faithful morphism $B \colon U \rightarrow G$ in $C$, there is a unique morphism $F:G \rightarrow Set$ such that there is a (2,1)-pullback diagram of the form
If $Set$ exists, it is typically called the universe of sets or groupoid of sets. A global element $F:G \rightarrow Set$ is typically called an indexed family, an element $A:* \rightarrow Set$ is typically called a set, and a set $A:* \rightarrow Set$ is inhabited if there exists a morphism $B:* \rightarrow [I, Set]$ such that the $A$ factors into $inhabited \circ B$. All these terms refer to the internal set theory of the (2,1)-category $C$.
The morphism $\chi_U$ is also called the classifying morphism of the discrete object $U$ and morphism $B:U \rightarrow G$.
In the (2,1)-category Grpd of groupoids and functors between groupoids, the discrete object classifier is the groupoids of sets and bijections (i.e. the groupoid core of Sets).
Last revised on January 3, 2024 at 15:42:23. See the history of this page for a list of all contributions to it.