(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
A partial function between two sets can be turned into a total function by adjoining a further element to and sending all that are not in the domain of definition of to this new value = “undefined” and the rest just to their value under . Conversely, every function with codomain corresponds to a unique partial function to whence is a ‘classifying object’ for these.
More generally, a partial function classifier or partial map classifier of an object in a category is a representing object for partial maps with codomain .
Let be a category with pullbacks. Recall that a partial map in is a span in which the map is a monomorphism. The subobject is called the domain of the partial map. Two partial maps are considered equal if they are related by an isomorphism of spans; in this way we obtain a set of partial maps .
We can compose a partial map with a map in an obvious way. We can also compose it with a map by pulling back the mono to . In this way becomes a profunctor from to itself. (In fact, it is the hom-set of another category with the same objects as .)
A partial map classifier for is an object together with an isomorphism
natural in . By the Yoneda lemma this means there is a universal partial map .
The existence of partial map classifiers for all objects in amounts to the existence of a right adjoint for the inclusion where the latter is the usual category of partial maps of .
Given a type , the partial function classifier is inductively generated by
and the partial order type family is simultaneously inductively generated by
a family of dependent terms
representing that each type is a proposition.
a family of dependent terms
representing the reflexive property of .
a family of dependent terms
representing the transitive property of .
a family of dependent terms
representing the anti-symmetric property of .
a family of dependent terms
representing that is initial in the poset.
a family of dependent terms
a family of dependent terms
representing that denumerable/countable joins exist in the poset.
In a Boolean extensive category (such as a Boolean topos), we can define the partial map classifier as , where is the terminal object. This is because in an extensive category, a map is equivalent to a decomposition of as a coproduct together with a map (the map being unique), and in a Boolean category every subobject of is complemented and hence induces such a coproduct decomposition. The universal partial map has domain the summand , on which it is the identity. Note that is also known as the maybe monad.
Partial map classifiers also exist in every elementary topos, but in the non-Boolean case they are harder to construct. Letting denote the top element, the dependent product is precisely the map classifying . To wit, with this definition,
Alternatively, in the internal logic, two ways of defining that more closely follow the classical construction are:
is a subobject of the power object consisting of the subsingleton subobjects of . In this case, the universal partial map has domain the set of singleton subobjects of , on which it is an isomorphism.
is the object of partial maps . In this case, the universal partial map has domain the set of partial maps which are total, on which it is an isomorphism.
Note that neither of these constructions is predicative. The second makes more sense in a higher category (or in its internal logic such as homotopy type theory).
In an intuitionistic context, still classifies something: namely partial maps whose domain of definition is a decidable subobject of .
In type theory one uses the partiality monad to treat general recursion as an algebraic effect. In this we we obtain a classifier for recursively enumerable subsets. Is this the first appearance? It is clear that this idea can be generalized to other classes of propositions.
In a topos, the partial map classifier of is injective. The canonical embedding shows accordingly that a topos has enough injectives!
In a topos, the subobject classifier coincides with the monomorphism .
In a topos, the assignment of to is functorial.
Section 1.2 of
A2.4 of the Elephant
For partial function classifiers in homotopy type theory:
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (abs:1610.09254)
Martín Escardó, Cory Knapp, Partial Elements and Recursion via Dominances in Univalent Type Theory (pdf)
Discussion for topological spaces:
Last revised on June 20, 2022 at 11:32:17. See the history of this page for a list of all contributions to it.