[Agda] defining coinductive types
pedagand at gmail.com
Wed Dec 18 20:02:35 CET 2013
> 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"
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
For the sake of completeness, I should also mention Pitts'
"Polymorphism is set theoretic, constructively", which I won't dare
More information about the Agda