Commit 2025-01-11 13:24 cdcfe3a4

View on Github →

chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) The names are now prefixed with Is. As a result, the definition of an abelian category Abelian only involve props in addition to the Preadditive instance. With this design, we may avoid diamonds for Abelian instance in some future works (e.g. the abelian category structure on the heart of a t-structure).

Estimated changes