These theories are intended as interfaces for high-level programming; this current collection includes implementations in particular using concrete relations, and a number of constructions, including quotients by (abstractions of) partial equivalence relations.

**RATH-Agda-2.0.* should work with Agda development versions
of December 2013 and later,
and corresponding versions of the standard library.**

When working with RATH-Agda, it is strongly recommended to set a fixed heap for the Agda process, running, for example:

time agda +RTS -K64M -S -M6G -H6G -RTS -i . -i $STDLIB(The “SomeTheory.lagda

`-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.)
Downloads:

**RATH-Agda-2.0.1**(2014-02-02)- RATH-Agda-2.0.1.pdf (1.9MB) 456 pages literate document output of all RATH-Agda-2.0.1 theories
- RATH-Agda-2.0.1.tar.gz (286kB; unpacked 1.8MB; about 35k lines of Agda source)

**RATH-Agda-2.0.0**(2014-01-08)- RATH-Agda-2.0.0.pdf (1.9MB) 456 pages literate document output of all RATH-Agda-2.0.0 theories
- RATH-Agda-2.0.0.tar.gz (286kB; unpacked 1.8MB; about 35k lines of Agda source)
- RATH-Agda-2.0.0_agdai.tar
(123.8MB
`.agdai`

files, which are already compressed)This is to be unpacked from the same place as RATH-Agda-2.0.0.tar.gz

This builds on RATH-Agda-2.0.1.

Downloads:

- MonCoAlg-0.1.pdf (815kB) 105 pages literate document output of all MonCoAlg-0.1 theories
- MonCoAlg-0.1.tar.gz
MonCoAlg-0.1 can be checked from source without first checking all of RATH-Agda-2.0.1, using the following commands in the otherwise empty download directory:

$ STDLIB=YourInstallationDirectoryOfTheAgdaStdLibrary/src $ tar xzf RATH-Agda-2.0.1.tar.gz $ tar xzf MonCoAlg-0.1.tar.gz $ cd MonCoAlg-0.1/ $ time agda +RTS -H11G -M11G -K128M -RTS -i . -i ../RATH-Agda-2.0.1 -i $STDLIB MonCoAlg0All.lagda

This will not work with much less than 10GB of heap. (Without contention for RAM, this may take around 40 minutes.)

**AContext-2.1**(2015-07-29)- Duality proof completed beween contexts with relational homomorphisms
and complete lower semilattices with meet-preserving homomorphisms.
(Final
`record`

assembly not yet checked by Agda; requires more than 52GB heap.)Downloads:

- AContext-2.1.pdf (1.2MB) 191 pages literate document output of the AContext-2.1 theories
- AContext-2.1_2up_letter.pdf (0.9MB), same as the above, but arranged for 2-up viewing (or printing on “Letter” paper).
- AContext-2.1.tar.gz (231kB)
contains not only the AContext-2.1 development,
but also the underlying OSGC and OCC base theories
belonging to RATH-Agda (and documented there)
— no download of RATH-Agda is necessary to use these
theories.
This development works with the current stable version of Agda, i.e., 2.4.2.3, and a matching version of the Agda standard library.

It also works with Agda development versions at least of mid-July 2015. (With these, in particular using

`--sharing`

, typechecking this development is much faster.)On my machine, checking this whole development via the entry point

`AContext2.lagda`

from scratch using the development version of Agda requires at least 8GB of heap, and takes about 14 minutes. Using Agda-2.4.2.3 requires at least 10GB of heap, and takes about 27 minutes.

**AContext-2.0**(2015-05-03)- Previous version: Mapping between contexts and complete lower semilattices established.
- AContext-2.0.pdf (0.9MB) 69 double pages literate document output of the AContext-2.0 theories
- AContext-2.0.tar.gz (161kB) contains not only the AContext-2.0 development, but also the underlying OSGC and OCC base theories belonging to RATH-Agda (and documented there) — no download of RATH-Agda is necessary to use these theories.

**AContext-1.0**(2014-01-08)- First version: Category of contexts with relational homomorphisms.
A first exploration of formalising the way contexts give rise to concept lattices in formal concept analysis (FCA).

This builds on RATH-Agda-2.0.0 and will also work with RATH-Agda-2.0.1.

Downloads:

- AContext-1.0.pdf (450kB) 25 pages literate document output of all AContext-1.0 theories
- AContext-1.0.tar.gz
AContext-1.0 can be checked from source without first checking all of RATH-Agda-2.0.0, using the following commands in the otherwise empty download directory:

$ STDLIB=YourInstallationDirectoryOfTheAgdaStdLibrary/src $ tar xzf RATH-Agda-2.0.0.tar.gz $ tar xzf AContext-1.0.tar.gz $ cd AContext-1.0/ $ time agda +RTS -H2G -M2G -K64M -RTS -i . -i ../RATH-Agda-2.0.0 -i $STDLIB Data/AContext/Category.lagda