Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added to partial function a new section Definition – General abstract with a brief paragraph on how partial functions form the Kleisli category of the maybe-monad.
That description of partial functions in terms of the monad $1 + -$ works in $Set$, and (I think off the top of my head) in any Boolean topos, but not more generally.
In the early days of topos theory, before the definition of topos became codified in the form best known today, people used to talk a lot about partial map classifiers. I haven’t checked to see what we have on that notion in the nLab.
In a general extensive category, the kleisli morphisms for the maybe monad will be the partial functions with complemented domain.
Yes, that’s the sharper way of putting it.
I had raised adding extensiveness in the other thread here.
Will try to put it into the entry. Only have one hand free though…
FWIW: partial map classifier
There is already stuff about this monad (but the constructive version, not the maybe monad) near the bottom of the page, under “The category of sets and partial functions”. But this doesn't actually discuss how it's a monad!
Ok, clearly partial function and partial map classifier and maybe monad need to be interlinked, and there is a query box from Emily on the former which should be answered. The “total functions $S_\bot\to T_\bot$ such that inhabited subsets of $T$ are assigned only to inhabited subsets of $S$” referred to at partial function must be the algebra maps for the partial map classfier monad, so that we are identifying $Set_\bot$ with the Kleisli category of that monad regarded as the subcategory of free algebras. However, it’s not immediately clear to me what a general algebra for this monad is in a constructive setting (classically, every such algebra is free).
A type-theoretic description of the PMC as “the set of subsets with at most one element” is
$A_\bot = \sum_{P:A\to Prop} isProp\Big(\sum_{a:A} P(a)\Big).$Am I right in thinking that this is equivalent to
$\sum_{U:Prop} (U\to A) \quad ?$If so, that at least gives a slightly more explicit description of its algebras.
I'm getting that those two expressions are describe equivalent sets in constructive set theory. If they both satisfy isSet in HoTT, then this means that they should be straight-up equivalent, yes?
Proposition 2.4.7 in [Sketches of an elephant, Part A] constructs the partial map classifier as $\Sigma_{\Omega} \Pi_{\top} A$, where $\top : 1 \to \Omega$ is the generic subobject. I suppose in type-theoretic notation this is
$\sum_{U : Prop} \prod_{x : \top (U)} A$and since the fibre $\top (U)$ is just $U$ itself, this is the type you describe.
I put in some reply to Emily.
Thanks Zhen! Toby, they are both sets as long as $A$ is, which is the case I was thinking of; otherwise the first is a set but the second is not. And I think the second is a more sensible PMC for non-sets.
What happens if we do the same construction for this constructive maybe monad? [Sorry, I don’t have the time now, I may come back later.] Also in type theory one considers the partiality monad where uses the “r.e. propositions”, of course this can be generalized to other classes of propositions.
And I think the second is a more sensible PMC for non-sets.
Agreed.
I’ve added a few more remarks to partial map classifier and partial function.
I don't understand this business about ‘the set of functions $P\to B$ whose domain $P$ is a subsingleton’. In particular, in classical mathematics, this describes a proper class! I know what it's supposed to mean, but I don't know any way to formalize it in a topos other than by turning it into the previous construction. Arguably, the proper way to formalize the previous construction in HoTT is to turn it into this, so there's not really a difference between them.
We can describe both of these, to be sure. But they don't really seem different to me. Certainly not internally to a topos.
I was trying to describe the two different definitions I gave above in #9. They are equivalent, as they must be, but they are different definitions.
I rewrote them so that they're more clearly in the language internal to a category. In particular, there's no quantification over arbitrary subsingleton objects, just subobjects of one terminal object.
But if I start being too explicit about how this looks in the internal language, then they start looking very similar again. (What is the object of partial maps $1 \rightharpoonup B$? Well, it's the object of subobjects of $1 \times B$ such that […], which is of course the same as the object of subobjects of $B$ such that [back to the first definition].) Maybe we should use an explicit reference to the dependent sum over the object of truth values?
Added to partial map classifier a remark on $B+1$ always classifying partial maps whose domain of definition is a decidable subset of the source.
@Toby: Sure, if you think that would make it clearer.
Added the use in type theory. I expect classifiers for different classes of partial maps have also been studied (open, closed domain …) But I do not know the references off hand.
The server seems to be having problems.
I added some stuff about the algebra of real-valued partial functions of one real variable, the one that's studied in high-school math, as analysed by Fred Richman.
I fixed the incorrect statement in the section http://ncatlab.org/nlab/show/partial+function#in_terms_of_the_maybe_monad which used to say that the domain of the partial function corresponded to the preimage of the extra disjoint point!
@Toby
I also added a statement that feels ’more constructive’, but is not quite there:
an element $x\in A$ is sent to $\ast$ by $\phi$ if and only if the original partial function is undefined at $x$.
I’d rather make a positive statement like “a partial function is defined at $x$ iff the corresponding partial function sends $x$ to a value in $B\subset M(B)$” where $M$ is the Maybe monad, since one doesn’t need to define the Maybe monad as $(-)\coprod \ast$. Or we don’t even need to phrase it in terms of Maybe: I would guess that $B \subset M(B)$ is not an iso, or perhaps that there is an element of $M(B)$ disjoint from $B$, is enough.
EDIT: oh, this all seems to be subsumed later down the page, with $Set_\bot$, where what I wrote as $M(B)$ is there called $B_\bot$, and is actually worked out.
I think that I made that phrasing better; you can't make it work constructively using that monad, but at least one can avoid double negations.
Thanks Toby, that’s much better!
Thanks!
1 to 27 of 27