Regular categories

Stream: Is there code for X?

[Robert Maxton]

Do we have the idea of a regular category, perhaps by some other name? We have typeclasess expressing that every mono/epi is regular, but I don't think that's the same thing.

[Joël Riou]

We have https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Shapes/RegularMono.html

[Robert Maxton]

Yes, that's the typeclass I was referring to :p.

[Robert Maxton]

A regular category is one where regular epis are effective and stable under pullback

[Joël Riou]

We also have docs#CategoryTheory.EffectiveEpi but I do not think this is what would solve your CW-complexes issues.

[Dagur Asgeirsson]

We have RegularEpi as well, and the fact that they agree with EffectiveEpi whenever the relevant pullbacks exist. We also have preregular categories (a definition invented for mathlib), and I think a preregular category with finite limits is at least very close to being a regular category