[Agda] running out of memory in formalization of category theory

[Nils Anders Danielsson]

On 2010-06-08 17:38, Dan Licata wrote:
> Is there a way to turn off eta equality to test this hypothesis?

Not without changing the implementation.

> I think I remember seeing something like "temporarily disable eta" in
> the change logs recently.

Ulf tested whether it would be useful to be able to selectively turn on
eta for records.

--
/NAD