search

agda / agda-categories

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

Remove broken, unused, AllProducts and IndexedProduct #377

Closed Taneb closed 1 year ago

Taneb commented 1 year ago

This construction was significantly weaker than its name suggested. See https://github.com/agda/agda-categories/issues/258#issuecomment-889119426 for proof that AllProducts was implied by Terminal. It is also unused.

Closes #258