<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div>It may be worthwhile to explore the alternative, and well documented, <br></div><div>RATH-Agda [0, 1] library. It is organised around monolithic pieces:</div><div>theories are structured about smaller and useful subtheories.</div><div>For example, categories are built upon the notions of semigroupoids</div><div>which are themselves quiet frequent. Moreover, the RATH library also</div><div>provides pleasent reasoning combinators to make some proofs easier</div><div>to read, type, and reason about. </div><div><br></div><div>I currently use the RATH-library on my Agda 2.5.1.1 and use it in-place/along-side</div><div>of the standard library as well! For the latter, the reason is that the RATH-Agda</div><div>library does a lovely job of prefixing the operator name to an associated property;</div><div>e.g., it uses `op-refl` rather than just `refl` and this is quiet helpful when one has</div><div>operators with similar properties and really avoids a lot of renaming hassle!</div><div>(It also provides subscripted versions of many operators.)</div><div><br></div><div>[0] RATH-Agda Homepage</div><div><a href="http://relmics.mcmaster.ca/RATH-Agda/">http://relmics.mcmaster.ca/RATH-Agda/</a><br></div><div><br></div><div>[1] Manual of RATH-Agda</div><div><a href="http://relmics.mcmaster.ca/RATH-Agda/RATH-Agda-2.0.0.pdf">http://relmics.mcmaster.ca/RATH-Agda/RATH-Agda-2.0.0.pdf</a></div><div>     <br></div><div><br></div><div> </div></div></div></div>