Pullback-stable regular epimorphisms

[ScriptRaccoon]

This PR adds the last remaining constitutent property of regular categories (cf. #343): having pullback-stable regular epimorphisms. For convenience, it is required that pullbacks exist.

Of course, the dual property, having pushout-stable regular monomorphisms, is added as well. It is the last remaining constituent property of coregular categories.

Various results about the two new properties are added as well. For example, every multi-algebraic category has pullback-stable regular epimorphisms. Also, every locally cartesian closed category with binary products has pullback-stable regular epimorphisms.

The two new properties are decided for most categories in the database. Moreover, existing (co)regularity proofs and implications have been reworked.

As part of this PR, it is also shown (thanks AI) that Unif is coregular (it has pushout-stable regular monos), but not regular (it does not have pullback-stable regular epis). This is just like Top, but the proof for coregularity is much more involved. In particular, all properties of Unif are now decided.

Also, it is shown that Met_∞ has pushout-stable regular monomorphisms, hence is coregular. In particular, all properties of Met_∞ are finally decided.

TODOs

(!) This should be merged soon, since rebasing becomes more and more difficult. Maybe handle TODOs in separate PRs. Alternatively, do not merge anything else for now that touches the data.

TODO. Try to decide the remaining unknown cases:

Decide pullback-stable regular epis for

• Sch

(but we already know that these are not regular, because limits / colimits are not sufficient)

Decide pushout-stable regular monos for

• LRS

For every one of these we equivalently need to decide if it is coregular. (Look at the ChatGPT analysis.)