Pullback-stable regular epimorphisms

[ScriptRaccoon]

This PR adds the last remaining constituent property of regular categories (cf. #343): having pullback-stable regular epimorphisms. For convenience, the existence of pullbacks is required as well*.

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

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

The two new properties have been decided for all categories in the database.

In addition, existing (co)regularity proofs and implications have been reworked (for example, the proof that Grp is not coregular is actually a proof that Grp does not have pushout-stable regular monos), and new (co)regularity results have been obtained (with the help of AI):

• Unif has pushout-stable regular monomorphisms and is therefore coregular. This is analogous to Top, but the proof is much more involved.
• Unif does not have pullback-stable regular epimorphisms and is therefore not regular.
• Met_∞ has pushout-stable regular monomorphisms and is therefore coregular. For this result, the regular monomorphisms have been classified (also in Met): they are isometric maps with closed image.
• LRS_R does not have pushout-stable regular monomorphisms and is therefore not coregular. For this result, the regular monomorphisms have been classified: they are topological embeddings with surjective stalk maps.

A nice consequence is that all properties of Unif and Met_∞ have now been decided. Also, both properties "regular" and "coregular" are decided for all categories in the database.

Some other non-trivial results from this PR (also obtained with the help of AI):

• the regular epimorphisms in Met_c are the surjective continuous maps whose codomain carries the "final metric topology" (not necessarily the final topology)
• Met_c does not have pullback-stable regular epis
• Sch_R does not have pullback-stable regular epis

The number of missing consistent combinations (displayed on /missing) increases from 259 to 264. The new ones are:

• locally cartesian closed ∧ ¬pullback-stable regular epimorphisms (example given at MSE/5150479)
• locally cocartesian coclosed ∧ ¬pushout-stable regular monomorphisms (dual to the previous one)
• pretopos ∧ ¬pushout-stable regular monomorphisms
• quotient object classifier ∧ ¬pushout-stable regular monomorphisms
• subobject classifier ∧ ¬pullback-stable regular epimorphisms

*Otherwise, it is not completely clear how to state the property, cf. #370; must a regular epi have all pullbacks, which are regular epis, or are only those pullbacks that exist required to be regular epis?