[Agda] RATH-Agda-1.0: Relation-Algebraic Theories in Agda

[Wolfram Kahl]

Dear Agda friends,

  I finally got around to putting together a first release of
my formalisations of what I like to call ``relation-algebraic theories'',
that is, theories of allegories, Kleene categories,
and related structures that permit, or better, invite, the kind of calculational
inclusion-chain reasoning typical for (heterogeneous) relation algebra.

See:

  http://relmics.mcmaster.ca/~kahl/RATH/Agda/

The theories come with a overview paper I am presenting next week at RAMiCS
in Rotterdam, the literate document view comprising all included theories,
and .agdai files for those with not much RAM (or not much patience  ;-).
(On amd64, you still need about 600MB of heap to just load the .agdai files
 up to the definition of allegories, and almost 1GB for division allegories...)


Cheers,

Wolfram