nLab partial map classifier

Idea

A partial function $f \colon A\rightharpoonup B$ between two sets can be turned into a total function $\overline{f} \colon A\to B_\bot$ by adjoining a further element $\bot$ to $B$ and sending all $a\in A$ that are not in the domain of definition of $f$ to this new value $\bot$ = “undefined” and the rest just to their value under $f$. Conversely, every function with codomain $B_\bot$ corresponds to a unique partial function to $B$ whence $B_\bot$ is a ‘classifying object’ for these.

More generally, a partial function classifier or partial map classifier of an object $B$ in a category $\mathcal{C}$ is a representing object for partial maps with codomain $B$.

Definition

Let $\mathcal{C}$ be a category with pullbacks. Recall that a partial map $A \rightharpoonup B$ in $\mathcal{C}$ is a span $A \leftarrow D \to B$ in which the map $D\to A$ is a monomorphism. The subobject $D \hookrightarrow A$ 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 $Par_{\mathcal{C}}(A,B)$.

We can compose a partial map $A\rightharpoonup B$ with a map $B\to B'$ in an obvious way. We can also compose it with a map $A'\to A$ by pulling back the mono $D\hookrightarrow A$ to $A'$. In this way $Par_{\mathcal{C}}(-,-)$ becomes a profunctor from $\mathcal{C}$ to itself. (In fact, it is the hom-set of another category with the same objects as $\mathcal{C}$.)

A partial map classifier for $B$ is an object $B_\bot$ together with an isomorphism

$$\mathcal{C}(A,B_\bot) \cong Par_{\mathcal{C}}(A,B)$$

natural in $A$. By the Yoneda lemma this means there is a universal partial map $B_\bot \rightharpoonup B$.

The existence of partial map classifiers $B_\bot$ for all objects $B$ in $\mathcal{C}$ amounts to the existence of a right adjoint for the inclusion $\mathcal{C}\hookrightarrow Par(\mathcal{C})$ where the latter is the usual category of partial maps of $\mathcal{C}$.

As a higher inductive-inductive type

Given a type $T$, the partial function classifier $T_\bot$ is inductively generated by

• a function $inj:T \to T_\bot$
• a term $\bot:T_\bot$
• a function $\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to T) \to T$

and the partial order type family $\leq$ is simultaneously inductively generated by

• a family of dependent terms

  $$a:T, b:T \vdash \pi(a,b):isProp(a \leq b)$$

  representing that each type $a \leq b$ is a proposition.

• a family of dependent terms

  $$a:T \vdash \rho(a):a \leq a$$

  representing the reflexive property of $\leq$.

• a family of dependent terms

  $$a:T, b:T, c:T \vdash \tau(a, b, c):(a \leq b) \times (b \leq c) \to (a \leq c)$$

  representing the transitive property of $\leq$.

• a family of dependent terms

  $$a:T, b:T \vdash \sigma(a, b):(a \leq b) \times (b \leq a) \to (a = b)$$

  representing the anti-symmetric property of $\leq$.

• a family of dependent terms

  $$a:P \vdash t(a):\bot \leq a$$

  representing that $\bot$ is initial in the poset.

• a family of dependent terms

  $$n:\mathbb{N}, s:\mathbb{N} \to T \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)$$

• a family of dependent terms

  $$x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\left(\prod_{n:\mathbb{N}}(s(n) \leq x)\right) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$$

representing that denumerable/countable joins exist in the poset.

Constructions

In a Boolean extensive category (such as a Boolean topos), we can define the partial map classifier as $B_\bot = B + 1$, where $1$ is the terminal object. This is because in an extensive category, a map $A\to B+1$ is equivalent to a decomposition of $A$ as a coproduct $D+E$ together with a map $D\to B$ (the map $E\to 1$ being unique), and in a Boolean category every subobject of $A$ is complemented and hence induces such a coproduct decomposition. The universal partial map $B+1 \rightharpoonup B$ has domain the summand $B$, on which it is the identity. Note that $B\mapsto B+1$ 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 $t : 1 \to \Omega$ denote the top element, the dependent product $t_*(B)$ is precisely the map $B_\bot \to \Omega$ classifying $B \subseteq B_\bot$. To wit, with this definition,

$$\begin{aligned} \mathcal{C}(A, B_\bot) &\cong \coprod_{p : A \to \Omega} \mathcal{C}/\Omega(p, t_*(B)) \\&\cong \coprod_{p : A \to \Omega} \mathcal{C}(t^*(p), B) \\&\cong \coprod_{A' \subseteq A} \mathcal{C}(A', B) \\&\cong Par_{\mathcal{C}}(A, B) \end{aligned}$$

Alternatively, in the internal logic, two ways of defining $B_\bot$ that more closely follow the classical construction are:

• $B_\bot$ is a subobject of the power object $\mathcal{P}B$ consisting of the subsingleton subobjects of $B$. In this case, the universal partial map $B_\bot \rightharpoonup B$ has domain the set of singleton subobjects of $B$, on which it is an isomorphism.

• $B_\bot$ is the object of partial maps $1 \rightharpoonup B$. In this case, the universal partial map $B_\bot \rightharpoonup B$ 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).

Remark

In an intuitionistic context, $B + 1$ still classifies something: namely partial maps $A \rightharpoonup B$ whose domain of definition is a decidable subobject of $A$.

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.

Properties

• In a topos, the partial map classifier $B_\bot$ of $B$ is injective. The canonical embedding $B\rightarrowtail B_\bot$ shows accordingly that a topos has enough injectives!

• In a topos, the subobject classifier $true:1\rightarrow\Omega$ coincides with the monomorphism $\eta_1:1\rightarrowtail 1_\bot$.

• In a topos, the assignment of $B_\bot$ to $B$ is functorial.

References

• F. Borceux, Handbook of Categorical Algebra - vol. 3 , Cambridge UP 1994. (sec.5.5)

Section 1.2 of

• Peter Johnstone, Topos theory, London Math. Soc. Monographs 10, Acad. Press 1977, xxiii+367 pp. (Dover reprint 2014)

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:

• Peter May, Johann Sigurdsson, Def. 1.3.6 in: Parametrized Homotopy Theory, Mathematical Surveys and Monographs, vol. 132, AMS 2006 (ISBN:978-0-8218-3922-5, arXiv:math/0411656, pdf)