[Agda] Re: Codata oddity

[Nils Anders Danielsson]

On Fri, Jun 6, 2008 at 3:16 PM, Nils Anders Danielsson
<nils.anders.danielsson at gmail.com> wrote:
>
> If we evaluate p we get refl, but if we replace the right-hand side of
> p with refl we get a type error, so we do not have preservation of
> types.

Apparently Coq has the same problem. See
http://pauillac.inria.fr/pipermail/coq-club/2008/003675.html.

-- 
/NAD