[Agda] Re: strict unit type

[Dan Doel]

On Sun, Apr 29, 2012 at 5:36 PM, Guillaume Brunerie
<guillaume.brunerie at gmail.com> wrote:
> I’m not sure how Agda works, though. I tried a few things, and in the
> context (u : unit), the normal form of u is u, but refl u is
> nevertheless accepted as an inhabitant of the identity type Id unit u
> tt, so it seems that convertibility is not defined as equality of
> normal forms in Agda.

Agda will not always display things eta expanded, or perform eta
expansion on everything; it tries to delay as much as possible. The
reason is that aggressively eta expanding everything causes serious
performance degradation.

-- Dan