[Agda] defining coinductive types

[Pierre-Evariste Dagand]

Hi Aaron,

> But I am asking about positive but not strictly positive recursive types.

I believe that the canonical example of such a beast is the functor
      T X = (X -> Bool) -> Bool
that, in predicative type theory, does not admit an initial algebra.
That much is said by Altenkirch & Morris in "Indexed containers"
([http://www.cs.nott.ac.uk/~txa/publ/ICont.pdf], p.5).

You might ask 'why?'. So did I. To which Peter Hancock replied with a
reference to Reynolds' "Polymorphism is not set-theoretic", where the
initial algebra of this functor plays a central rôle (bottom of
p.149). An approximate tl;dr of this paper (which should be taken with
a pinch of salt) seems to be that: if you've the initial algebra of
the ill-fated functor T, you cannot have a set theoretic model of your
logic.

For the sake of completeness, I should also mention Pitts'
"Polymorphism is set theoretic, constructively", which I won't dare
comment.

Cheers,

--
Pierre