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.
- Agda 2.6.1
- agda-stdlib 1.3
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.