Paul Taylor wrote in part:
Toby Bartels said that the "UNDERLYING-SET AXIOM" in ASD is impredicative. This is correct, but I introduced this axiom as a "straw man". First, in order to say exactly what is needed to make ASD equivalent to (locally compact locales over) an elementary topos.
OK, that's pretty much what I thought.
Second, to make the point that a great deal of mainstream mathematics is computable and does NOT require underlying sets. I see the main thread of ASD as being about a computable theory.
I hope you won't mind if I take this opportunity to ask something that I've been idly wondering about ASD lately, and which is related to this thread (even the Cantor set). That is: to what extent does ASD have inductive and coinductive objects; in other words: to what extent do polynomial functors have initial algebras and final (terminal) coalgebras? Of course, N is put in by hand as the initial algebra of X |-> 1 + X. And I know that you've constructed Cantor space as 2^N (through a bit of argument since exponentials don't always exist) and the proof that this is the final coalgebra of X |-> 2 x X goes through. But the final coalgebra of X |-> N x X would be Baire space, which is not locally compact, so we don't expect that to work. My intuition is that polynomials with overt discrete coefficients should have overt discrete initial algebras, while those with compact Hausdorff coefficients should have compact Hausdorff final coalgebras. Have you any thoughts about that question?
[Toby] has said, for example * [...] * Similarly, if you remove identity types from intensional type theory (so breaking the justification of countable choice), you can still justify the fullness axiom and so construct the Dedekind reals (albeit not literally as sets of rational numbers). * [...] * But the Dedekind reals, as far as [he] can tell, do not; excluded middle, power sets, fullness, or countable choice would each do the job, but you need ~something~.
I would challenge someone to consider the last of these questions seriously, maybe taking a hint from the second.
I'd be interested to hear if anybody has done ~any~ work on the second: intensional type theory without identity types. It seems to me to work if done in the style of Thierry Coquand (with inductive types and dependent products as the main constructions) but not if done in the style of Per Martin-Löf (with W-types and dependent and finitary products and sums). I should probably say something about what categories would serve as syntactic models of such a type theory, but I never fully worked that out. --Toby