The category of metric spaces has no regular subobject classifier

[ScriptRaccoon]

This PR implements #304 and shows that

• Met and Met_∞ have no regular subobject classifier
• PMet has a regular subobject classifier
• the regular monomorphisms PMet are the injective isometric maps

The regular monomorphisms in Met and Met_∞ are still not understood.

The number of unknown (category, property)-pairs goes down from 72 to 69.

Thanks @dschepler for providing the proofs!

---

After merging, I realized that it also brings down the number of missing combinations from 409 to 399. Namely, PMet (or its dual) newly witnesses:

- regular subobject classifier ∧ ¬binary copowers
- regular subobject classifier ∧ ¬binary coproducts
- regular subobject classifier ∧ ¬cokernel pairs
- regular subobject classifier ∧ ¬equalizers of cokernel pairs
- regular subobject classifier ∧ ¬pushouts
- regular quotient object classifier ∧ ¬binary powers
- regular quotient object classifier ∧ ¬binary products
- regular quotient object classifier ∧ ¬kernel pairs
- regular quotient object classifier ∧ ¬coequalizers of kernel pairs
- regular quotient object classifier ∧ ¬pullbacks

The initial goal of this milestone is reached, but I think we can do better.