agda / agda-categories

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

Discrete adjoint #297

Closed JacquesCarette closed 3 years ago

JacquesCarette commented 3 years ago

This doesn't yet meet challenge #41 but it is progress in that direction. It does seem that the challenge is indeed feasible.

The main thing done here is to properly define DiscreteCategory. A bunch of other things were moved around to be more precise (i.e. mostly add Strict to the name as appropriate).