[Agda] Are there unicorns in Agda?

[Martin Escardo]

On 11/02/12 23:33, Martin Escardo wrote:
>The argument I gave  doesn't use syntax or models.

This is TRUE.

However, they are motivated by models (and definitely not by syntax).

Martin