Unpointed topologies with no backwards compatibility

[zstone1]

Separates the Pointed structure from TopologicalType. Definitely not backwards compatible, but most people shouldn't notice since once we hit pseudometric_zmodType we put Pointed back in there anyway. See #1191 for a previous attempt.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[zstone1]

Note this has some catastrophic performance regression in 8.18. From my little debugging, it appears the trivial tactic is slow when there are topologies/pointed topologies around. Sometimes adding a /= fixes it, so something pretty deep and bad is happening. I'm sure it's easy to fix with the right hint or instance, but I have no idea what that would be.

Performance is unaffected on 8.19 and 8.20, though. So it probably makes sense to wait if we're planning on dropping 8.18 support soon anyway.

[CohenCyril]

Let's drop 8.18 asap and merge.