Awesome

Category Theory in Agda

This is a formalisation of some standard notions of category theory in Agda. Some of the definitions are stolen from John Wiegley's similar effort in Coq. Don't expect anything to be 'production-ready' in any sense.

Dependencies

• Agda 2.6.1
• agda-stdlib 1.3