free algebras in ASD

[Paul Taylor <pt09@PaulTaylor.EU>]

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.