During the discussion on Dedekind vs Cauchy reals, Toby Bartels asked me
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?
In fact, what I have to say about this (in the setting of the existing established theory for locally compact spaces) is little more than Toby's "intuition". The existence of these spaces would follow from the limit--colimit coincidence, which is sketched in Remark 10.16 of "Geometric and higher-order logic in ASD" www.PaulTaylor.EU/ASD/loccpct#geohol I did have in mind (in 2003, largely as a way of avoiding doing any real analysis) to formulate a language for free algebras and cofree coalgebras based on this idea. I then spent half a year on the construction of the free monoid ("set of lists") and free semilattice ("finite powerset") on an overt discrete object, ie writing the paper "Inside every model of ASD lies an arithmetic universe" www.PaulTaylor.EU/ASD/loccpct#insema At no point did this present any insuperable obstacles, but it did keep presenting obstacles, so I got heartily sick of discrete maths in ASD, and was then amenable to being persuaded to do some analysis. The symmetry between => T /\ = some overt discrete free algebra and <= F \/ != all compact Hausdorff cofree coalgebra is very strong in this, but not perfect, because N is overt discrete Hausdorff not compact 2^N is compact Hausdorff not discrete overt I have not managed to isolate convincingly the precise point where the symmetry breaks down. For example, my paper "Computably based locally compact spaces" www.PaulTaylor.EU/ASD/loccpct#comblc investigates the formula phi x = Some n:N. A_n phi /\ beta^n x that captures the way in which locally compact spaces and locales have bases of compact/open pairs. (Note that the spatial and localic cases are different -- in an interesting topological way, not just regarding Choice.) So I thought, "what if" we write down the dual formula phi x = All k:K. A_k phi \/ beta^k x which we think of as a system of overt/closed pairs indexed by a compact Hausdorff space K. (Having used the phrase "dual base" already, I called this a "canopy".) It turns out that every locally compact space has a canopy. This is proved in the notes "Tychonov's theorem in ASD". www.PaulTaylor.EU/ASD/misclc#tyctas which also contain the construction of Cantor space that Toby mentioned. All of this is, as I said, within the existing established theory of locally compact spaces. Extending the theory beyond this is something that has occupied my mind for some time without coming to any satisfactory conclusions. However, the "equideductive logic" that arises in any CCC with all finite limits is very promising as a framework. I have given three lectures about this, www.PaulTaylor.EU/slides/ and described in in the final section of "Foundations for Computable Topology" www.PaulTaylor.EU/ASD/foufct/ Paul Taylor PS The transfer of my website and email to a new hosting company is now complete. (PrimeXeon is a small outfit in Cambridge that provides intelligent helpful personal service for a mere 20 pounds per annum.) There were brief technical and admin problems over the weekend (I didn't understand MX records) that may have resulted in a failure to deliver mail to me. So if you tried to contact me on Sunday or Monday, please send your message again.