Categoric.*: Semigroupoids, categories, ordered categories with converse (OCCs), allegories, collagories, domain, residuals, restricted residuals, division allegories.
Relation.Binary.Heterogeneous.*: Heterogeneous binary relations, similar to AoPA, but universe-polymorphic and using standard library material where appropriate.
Data.Algebra.*: One view of parts of universal algebra.
It is strongly recommended to set a fixed heap for the Agda process, running, for example:
time agda +RTS -K64M -S -M12G -H12G -RTS -i . -i /var/tmp/AGDA/lib-0.5/src SomeTheory.lagda(The “
-K64M” flag increases also the stack size, which is necessary for typechecking some of the theories. “
-S” prints run-time garbage collection and heap usage information.)
.agdaifiles, which are already compressed)
This is to be unpacked in the same place as RATH-Agda-1.0.tar.gz:
tar xzf ~/Downloads/RATH-Agda-1.0.tar.gz tar xf ~/Downloads/RATH-Agda-1.0_agdai.tarFor Agda-2.2.10, the
.agdaifiles need to be more recent than the corresponding source files, otherwise it will typecheck again.
In particular the theories in
require large working memory.
I would not expect to be able to typecheck all of them (even in
individual Agda runs) with less than 3GB heap space;
most recently the the smallest heap I tried (successfully) was 6GB.