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.2 works only with Agda-2.5.2, released December 2016
(and presumably
with sufficiently recent development versions of Agda)
and corresponding versions of the standard library.**

(RATH-Agda-2.0.* should work with Agda versions of December 2013 and later, but definitely not with Agda-2.5.2 anymore.)

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 .(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.2**(2017-01-16)- RATH-Agda-2.2.pdf (2.4MB) 585 pages
literate document output of all RATH-Agda-2.2 theories
RATH-Agda-2.2_2up_letter.pdf, same as the above, but arranged for 2-up viewing (or printing on “Letter” paper).

- RATH-Agda-2.2.tar.gz (355kB; unpacked 2.7MB; about 40k lines of Agda source)

- RATH-Agda-2.2.pdf (2.4MB) 585 pages
literate document output of all RATH-Agda-2.2 theories
**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

- CoalgebraCollagories-0.1.pdf (570kB) 69 pages literate document output of the CoalgebraCollagories-0.1 theories
- CoalgebraCollagories-0.1_2up_letter.pdf, same as the above, but arranged for 2-up viewing (or printing on “Letter” paper).
- CoalgebraCollagories-0.1.tar.gz (63kB)
— this depends
on RATH-Agda-2.2 from above.
If RATH-Agda-2.2 is properly installed as a library, then the following should be sufficient to check this development:

tar xzf CoalgebraCollagories-0.1.tar.gz cd CoalgebraCollagories-0.1/src agda +RTS -S -A128M -K64M -M6G -H6G -RTS -i . CoalgebraCollagoriesAll.lagda

Otherwise, also supply the path to RATH-Agda-2.2:agda +RTS -S -A128M -K64M -M6G -H6G -RTS -i . -i YOURBASEDIR/RATH-Agda-2.2/src CoalgebraCollagoriesAll.lagda

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