[Agda] Re: 'categories' library in 2.5.1.1

[Musa Al-hassy]

It may be worthwhile to explore the alternative, and well documented,
RATH-Agda [0, 1] library. It is organised around monolithic pieces:
theories are structured about smaller and useful subtheories.
For example, categories are built upon the notions of semigroupoids
which are themselves quiet frequent. Moreover, the RATH library also
provides pleasent reasoning combinators to make some proofs easier
to read, type, and reason about.

I currently use the RATH-library on my Agda 2.5.1.1 and use it
in-place/along-side
of the standard library as well! For the latter, the reason is that the
RATH-Agda
library does a lovely job of prefixing the operator name to an associated
property;
e.g., it uses `op-refl` rather than just `refl` and this is quiet helpful
when one has
operators with similar properties and really avoids a lot of renaming
hassle!
(It also provides subscripted versions of many operators.)

[0] RATH-Agda Homepage
http://relmics.mcmaster.ca/RATH-Agda/

[1] Manual of RATH-Agda
http://relmics.mcmaster.ca/RATH-Agda/RATH-Agda-2.0.0.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161102/0ffda2ba/attachment.html