RATH-Agda: 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