Met_c is not regular

[ScriptRaccoon]

There are currently two categories for which it is not known whether they are regular: the category of schemes and the category of metric spaces with continuous maps. This PR settles the second case and proves* that Met_c is not regular.

Specifically, it proves that there is a morphism $f : X \to Y$ whose kernel pair $X \times_Y X \rightrightarrows X$ does not have a coequalizer. Hence, this provides an easier proof that quotients of congruences do not exist. As a result, the lemma in monic-sequential-colimits-via-congruence-quotients.md is no longer needed. However, I have not deleted it yet.

*The proof was found with Google Gemini and then formulated in my own words.

[ScriptRaccoon]

@dschepler What shall we do with content/monic-sequential-colimits-via-congruence-quotients.md? (You have added this lemma back then, but right now, it is not used anymore.)

[ScriptRaccoon]

@dschepler On the other hand, the alternative proof that I have just added suggests that we might be able to generalize the lemma:

Let $C$ be a countably extensive category in which every kernel pair has a coequalizer. Then $C$ has colimits of sequences of monomorphisms.

is this true? Then the 2nd assumption is satisfied for every regular category, which then can be used to show that Met_c is not regular, and also that it doesn't have quotients of congruences. (To make all of this even more elegant, the property "every kernel pair has a coequalizer" needs to be added to the database; and while we are at it, also "regular epis are pullback-stable", so that the property "regular" is completely decomposed. But not in this PR.).

[dschepler]

I don't know about that generalization. As far as I can tell, the alternate proof depends on being able to find a cocone of the sequence such that each map in the cocone is a monomorphism - such as your $\ell^2$. In the general situation of my lemma, or in the general situation of a countably extensive category in which every kernel pair has a coequalizer, I don't know how you would do that.

As for the question about what to do with my result if it's no longer used, I don't have strong opinions either way. I do find it an interesting generalization of the explicit construction of sequential colimits in Set, but I'm not too attached to keeping it in the database. (And if we remove it, we can presumably always restore it from history if it turns out we need it again.)

[ScriptRaccoon]

Thank you for the feedback!