search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
740 stars 67 forks source link

Use : Set explicitly instead of relying on inductive minimization #128

Closed SkySkimmer closed 11 months ago

SkySkimmer commented 1 year ago

As minimization to set is disabled relying on inductive minimization means relying on bugs.

SkySkimmer commented 1 year ago

Please merge

SkySkimmer commented 1 year ago

Ping

jwiegley commented 11 months ago

Thank you! I always like expressing what is required minimally and explicitly, so this is a very satisfying change to me.