(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, or, as is a groupoid with a category structure, more commonly known as the category of sets.
Last revised on November 19, 2022 at 01:01:36. See the history of this page for a list of all contributions to it.