Start a typeclass hierarchy of topological properties

[Columbus240]

By implementing topological properties as typeclasses we can let Coq automatically infer properties. This way for concrete topological spaces we only have to prove their strongest properties (normality, metrizability) and Coq will infer the rest when we need them. Currently only separation axioms and metrizability are implemented as classes in this branch.

I haven't considered all possible consequences of this design decision. Such inference is very useful, though typeclasses are just one way of doing it. Are there other feasible approaches? Will the resulting typeclass hierarchy break the inference algorithm, if too many topological properties and relations are added? Applying the hierarchy is a bit wonky. Consider TietzeExtension.v#L651-L652. In the proof we want to use that RTop is T₁. Ideally we would only write apply T1_sep and be done with it. Now I had to explicitly name RTop and invoke the inference algorithm with typeclasses eauto.

Something I couldn't do with my approach: Let "hereditary" be a predicate for topological properties. Then how can I make Coq automatically apply hereditary-ness? Currently such instances have to be written manually and are separate from any Coq-internal predicate "hereditary".

[Columbus240]

Now I do not think, that the benefit of the automation is worth the added complication of a typeclass hierarchy. It is rarely hard to manually complete the proofs.