search

agda / agda-categories

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

the naturality conditions for ann and distrib were missing. #373

Closed JacquesCarette closed 1 year ago

JacquesCarette commented 1 year ago

So this adds them. And a partial refactoring to use variables.

JacquesCarette commented 1 year ago

(Asking multiple people for review because this change is blocking me on other work that I'm doing, so I'd like to have this merged sooner rather than later)