Category Theory in Agda

March 17, 2020 ยท View on GitHub

Build Status

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