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.
Is it in fact true that the actual partial map classifier is this free omega-cpo? I don’t think that is actually what is proved by the cited paper (https://arxiv.org/pdf/1610.09254.pdf).
What they define in that paper is the free pointed $\omega$-cpo on a type. But the free pointed omega-cpo on a type in the sense of this paper need not be that type’s partial map classifier, although I believe in SET they coincide. In particular, the partial map classifier of a type is always directed-complete but I think this free $\omega$-cpo (which they define as a kind of free cocompletion under $\omega$-chains and a bottom element) is probably not directed-complete unless I am missing something.
If I wanted to show that the actual partial map classifier was the free pointed omega-cpo, I would need to show (in particular) for any two strict omega-continuous maps $h, h' : Lift(A) \to X$, we have $h=h'$ if they agree when restricted to $A$. I would think that to prove this, I would show every element $x:Lift(A)$ is a colimit that is preserved by $h,h'$. The diagram in question is indexed in $1 + \{* \mid x{\downarrow}\}$, and given by the inequality $\bot \leq \eta(x!)$. It is important that the points of this diagram are either $\bot$ or lie in the image of the unit $\eta:A\to Lift(A)$. Such a diagram could be presented by an $\omega$-chain if the law of the excluded middle held, but I don’t see how to do it otherwise.
It seems that it might be possible to repair the claim if $\omega$ were replaced by some completion, such as the “upper naturals”. In fact, I would say that the correct definition of an $\omega$-cpo in a topos is not given using the natural numbers object, but are instead defined by iterating the real partial map classifier as in the work of Marcelo Fiore, Gordon Plotkin and John Power https://homepages.inf.ed.ac.uk/gdp/publications/Cuboidal.pdf.
In particular, in SET it just so happens that the partial map classifier is $-+1$, so if you take the initial algebra of this functor you get $\mathbb{N}$. This does not happen in an arbitrary topos; the correct figure shape for an “$\omega$-chain” is obtained by considering the initial algebra for the real partial map classifier functor.
The page partial map classifier also contains the same false claim.
Perhaps it would be worth mentioning at both of these pages that there is more than one notion of “partial map”, which I think is the source of the confusion. The rest of the page partial map classifier is about classifiers for the topos-theoretic notion of partial map, where the domain can be an arbitrary subobject, whereas the ADK paper is about a more computational notion of partial map, where the domain is a “computable” subobject and hence can be expected to be characterized in countable terms. Does that seem right to you?
Oh boy… Thank you for noticing that, Mike! I think I agree with your proposed fix, but even if we do that that I feel there is a “missing proof” that this HIT construction actually gives rise to a dominance for which it is the partial map classifier.
One thing that is leading to confusion here is that this HIT construction is about constructing a pointed omega-cpo in the order-theoretic sense — meaning that the corresponding dominance would be a dominance on the category of (not-necessarily-pointed) omega-cpos, rather than on the category of types (sets, etc.) in which this thing is computed. So this is opening up a big can of worms, and I am wondering if it would be better to simpler delete this HIT from the partial map classifier page, and keep the example on quotient inductive type only.
Since you kept the exact same reference that the Anonymous OP thought proves the claim you say is wrong, maybe good to be more specific about what that reference really claims. I assume it’s about section 3.2 there? I have added (here) that pointer (and also added publication data and fixed the publication year), so now the pointer reads Altenkirch, Danielsson, and Kraus 2017, §3.2.
1 to 7 of 7