Many terms in 08-families-of-maps.rzk.md seem to be named using an outdated naming scheme.
For example the name total-equiv-family-of-equiv is written "conclusion-last" and is used for what I believe should be called is-fiberwise-equiv-is-total-equiv or is-family-of-equiv-is-equiv-total-map or some variation thereof.
Some names follow the "conclusion-first" paradigm, but mix up equiv and is-equiv.
For example family-equiv-total-equiv takes a family of maps and an is-equiv (total-map), but returns not fiberwise is-equiv, but rather actual fiberwise equivalences Equiv. It should probably be called something like family-equiv-is-equiv-total-map.
I was a bit scared to just run off on my own and try to clean up the document, since a) it is long and b) probably many other things rely on it.
So what is the best policy for this? As a preliminary measure, one could add properly named synonyms for the most important "outward facing" terms so that at least the dirt is contained until one can do a proper project-wide cleaning.
Many terms in
08-families-of-maps.rzk.mdseem to be named using an outdated naming scheme.For example the name
total-equiv-family-of-equivis written "conclusion-last" and is used for what I believe should be calledis-fiberwise-equiv-is-total-equivoris-family-of-equiv-is-equiv-total-mapor some variation thereof.Some names follow the "conclusion-first" paradigm, but mix up
equivandis-equiv. For examplefamily-equiv-total-equivtakes a family of maps and anis-equiv (total-map), but returns not fiberwiseis-equiv, but rather actual fiberwise equivalencesEquiv. It should probably be called something likefamily-equiv-is-equiv-total-map.I was a bit scared to just run off on my own and try to clean up the document, since a) it is long and b) probably many other things rely on it.
So what is the best policy for this? As a preliminary measure, one could add properly named synonyms for the most important "outward facing" terms so that at least the dirt is contained until one can do a proper project-wide cleaning.