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 with terminal object , interval object , and finite (2,1)-pullbacks, a discrete object classifier is a morphism whose target is a nonterminal object and whose source is the internal hom-object such that for every faithful morphism in , there is a unique morphism such that there is a (2,1)-pullback diagram of the form
If exists, it is typically called the universe of sets or groupoid of sets. A global element is typically called an indexed family, an element is typically called a set, and a set is inhabited if there exists a morphism such that the factors into . All these terms refer to the internal set theory of the (2,1)-category .
The morphism is also called the classifying morphism of the discrete object and morphism .
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.