Re: Dedekind versus Cauchy reals

[Toby Bartels <toby+categories@ugcs.caltech.edu>]

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