zstone1

I'd be happy to make an attempt at porting the rest. I have some free time coming up, so I should be able to make some progress. What would help...

Yeah, I'd love to help here. A couple things - Let me know what day works. I'm taking the next couple weeks off work anyway, so I'm pretty free. -...

@CohenCyril @affeldt-aist This is both a breaking change, and a restructuring of the hierarchy for topology stuff. However, by the time topology and lmodule merge in `normedtype.v`, the change is...

Yeah, backwards compatibility is usually worth the effort. This approach sounds feasible, but more than just the name of `topologicalType` changes. All the factories change too. I'll have to mess...

So I think the nicest approach to backwards compatability is to define ``` HB.structure Definition UnpointedFiltered (U : Type) := {T of Choice T & isFiltered U T}. HB.structure Definition...

Using the modules is fine for defining the hierarchy. One annoying issue is it doesn't put `nbhs` into scope because there are no top-level structures with `isFiltered`. That's easily fixed...

I'm encountering an HB issue I don't understand. I keep getting seeing ``` join_UnpointedPseudoMetric_PseudoMetric_between_topology_JustPseudoMetric_and_UnpointedUniform_Uniform ``` appear in the goals, which breaks all the `simple apply`s from the hints and seems...

Coming back to this after many months, I'm not sure how much effort with trying to make this backwards compatible. My recollection is - Several proposed hierarchy builder features would...

I've updated #1312 with more explicit instructions, and a bit of additional cleanup.

With https://github.com/math-comp/analysis/pull/1312 merged, this is now redundant.