[Agda] Agda's coinduction incompatible with initial algebras

[Peter Hancock]

On 04/10/2011 21:41, Martin Escardo wrote:
>
> In any category, for any endo-functor that has a both an initial
> algebra and a final co-coalgebra, there is a canonical map from the
> initial algebra to the final co-algebra. If this morphism is an
> isomorphism, then this is called a bi-free algebra (Peter Freyd
> originally called this a hermafrodite algebra). Freyd calls a
> category "algebraicly compact" if "every" endo-functor has a bi-free
> algebra. (Domains with strict continuous maps are algebraicly compact
> with respect to continuous endo-functors.)
>

Thanks, I've never appreciated that was what "algebraically compact" meant.
What on earth has that got to do with compactness?
The imagery of bi-free hermaphrodite algebras is exciting,
but the reality is more tedious and squalid.  Such a category is satanic harlotry
(as the Rev. Ian Paisley might have said).

The property reminds me of
   *properties like "Delta11", meaning having both a Pi11
     (inductive) and a Sigma11 (coinductive) form.
   * unique solution theorems like Banach's.

>
> It seems that you have shown that this extension of Agda with
> co-inductive types is actually an algebraicly compact extension of
> Agda.
>

I have no idea what is going on with Andreas's example, or even what
Agda's coinduction facilities actually are, though I do know they
use musical notation.  Perhaps the problem is that not enough
musical notation is being used, and we ought to have the natural sign,
staves, clefs, time-signatures and everything.  With metronome markings.

Hank