agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

add diagrammatic composition #316

Closed tetrapharmakon closed 2 years ago

tetrapharmakon commented 2 years ago

diagrammatic composition of morphisms, i.e.

f ; g : A --f--> B --g--> C

tuns out to be useful in some proofs, and it usually makes very fast the process of dualising a thing into a co-thing (just put a co- in front of names, and replace \circ with ; -which, again, is U+FF1B not U+003B)