Relation-Algebraic Theories in Agda


The basic category and allegory theory library of the RATH-Agda project, containing (only sporadically truly) literate theories ranging from semigroupoids, which are “categories without identities”, to “action lattice categories”, which are division allegories that are at the same time Kleene categories (i.e., typed Kleene algebras), including also monoidal categories.

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 . 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.)


Collagories of Coalgebras (2017-01-17)


MonCoAlg-0.1 (2014-02-02)

A first exploration of coalgebras with their functor factored over a monad, and coalgebra homomorphisms being Kleisli morphisms satisfying a modified commutativity condition.

This builds on RATH-Agda-2.0.1.


Order Theory and Concept Lattices in Ordered Categories Without Meets, Formalised in Agda

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.)


AContext-2.0 (2015-05-03)
Previous version: Mapping between contexts and complete lower semilattices established.
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.


Wolfram Kahl