This a summary issue to try to gather together things we have perhaps wished could change, but needed a breaking v3.0 to justify/permit, and in the spirit of having a uniform vocabulary parametrised by various notions X cf. this comment on #3052 for the analogous state of affairs under Algebra:
- In
Definitions:
- In
Structures:
- In
Bundles:
Anything else?
This a summary issue to try to gather together things we have perhaps wished could change, but needed a
breakingv3.0 to justify/permit, and in the spirit of having a uniform vocabulary parametrised by various notionsXcf. this comment on #3052 for the analogous state of affairs underAlgebra:Definitions:Totalto becomeLinearMisnomer:Relation.Binary.Definitions.Total#453Structures:Is{Dec}StrictPartialOrderto becomeIs{Dec}StrictOrder(it would only yield a partial order onceStrictToNonStrictgets applied...)Is{Dec|Strict|DecStrict}TotalOrderto becomeIs{Dec|Strict|DecStrict}LinearOrdercf. aboveIs{Partial}Equivalenceto become an alias forIs{Partial}Setoid?Linear, so we should try to get our story straight!Bundles:StructuresabovePosetto become an alias for (new)PartialOrdercf. theLatticerenamings undertaken a while back Problems with change ofSemilatticeoperation name #2166 / Fixes #2166 by fixing names inIsSemilattice#2211Anything else?