Re: free algebras in ASD

[Paul Taylor <pt09@PaulTaylor.EU>]

Toby Bartels and I have been discussing the relationship
between
     1-categorical ideas such as free algebras and cofree coalgebras
and
     2-level ideas such as overt discrete and compact Hausdorff.

It does seem to me to be a good question to ask why these relationships
hold, and why they break down.   Such questions arise in traditional
formulations of topology, in which other people may have some intuition.

I observed that
      N   is   overt    discrete    Hausdorff      not compact
    2^N   is   compact  Hausdorff   not discrete   overt
which Toby attributed to the fact that N is the free algebra for +1
whereas 2^N is the cofree coalgebra for a functor that is not directly
analogous.

I don't think the particular functors are very important, as (some of)
these properties hold of free algebras and cofree coalgebras in general.

So, a free algebra is
  - overt       because we can enumerate its (raw) terms,
  - discrete    because we can enumerate (proofs of) its equations,
  - not compact because there are infinitely many raw terms.

I don't have much experience of cofree coalgebras, but those that
do could probably formulate a similar argument for why they are
compact and Hausdorff.

N is peculiar in being Hausdorff (ie it has decidable equality).
This is because its theory is very simple.   Other free algebras
(my usual example is "combinatory algebra", with S and K) do not
have decidable equality.  Likewise, cofree coalgebras are not
discrete.

***** Why is Cantor space overt?
***** Do other cofree coalgebras have this property?

That would explain these particular failures of symmetry, but

***** Why does this relationship between the 1- and 2-level ideas
***** hold, and why is it this way round?

ASD might make things clearer here.   Its 1-level theory, like that
of an elementary topos, is not self-dual.   Toby observed that the
symmetry between free algebras and cofree coalgebras is only partial.
The ideas have long been well known in category theory, alhough,
if you go through the exactness properties of a pretopos, several
of them do actually hold for the dual category too.

The 2-level theory in ASD is quite interesting before we introduce
the axioms that break the duality.   These are:
- N is overt but not compact
- Scott continuity.

As I mentioned before, I tried a bit to develop things with dual ideas,
in particular starting from Cantor space instead of N.   I suspect that
there is a dual formulation of Scott continuity, although I couldn't
see what it is.  So I don't think that that's where the asymmetry lies.

I suspect that the symmetry is broken by the "convention" that
- N is overt but not compact
ie it has a quantifier, and we ("arbitrarily") call this "existential".

Paul Taylor