search

agda / agda-categories

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

Improve level polymorphism in one place. #380

Closed JacquesCarette closed 11 months ago

JacquesCarette commented 11 months ago

@xplat noticed that the product construction could have more general Levels. Also use variables a bit more while at it.