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

[Nils Anders Danielsson]

On 2010-06-03 11:43, Conor McBride wrote:
> Or is it that treatments of type theory tend to live in the
> inductively defined fragment, which is less eta-expandable?

Christian Sattler had problems when formalising category theory in Agda,
so he tried replacing all records with single-constructor data types.
Apparently he managed to finish another two definitions or so before
performance was a problem again (using Agda 2.2.4 or 2.2.6, I believe).
In other words, eta for records is not the sole culprit.

--
/NAD