RATH-Agda

Relation-Algebraic Theories in Agda

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

Downloads:

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.

Downloads:

AContext-1.0 (2014-01-08)

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:


Wolfram Kahl