search

agda / agda-categories

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

Properties of distributive categories #410

Closed Reijix closed 8 months ago

Reijix commented 8 months ago

I've added some properties of the distribution isos in Categories.Category.Distributive that I am using in my personal project.

Im very open for naming suggestions for these properties, the current names might not be that good.

I also thought about putting them in Categories.Category.Distributive.Properties but it seems to me that as soon as you are working with distributive categories you will need (some of) these helpers.

JacquesCarette commented 8 months ago

Should have said: really nice work. I do want to pull this in!

Reijix commented 8 months ago

Good point, I moved the properties to Categories.Category.Distributive.Properties.