Recent work in Algebra wrt 'sub'algebras (#2852 , #2854 , #2855 , #2859 , #2863 ...) exposes that, at least for Algebra.Morphism.MagmaMonomorphism, certain properties make spurious appeal to the underlying isMagma property (which exposes ∙-cong), when no appeal is made to ∙-cong... so the dependency in the anonymous module is bogus.
Fixing this in any sensible way, however, will be a breaking change, unless we regard this as a bug fix?
UPDATED: ugh. We need setoid, but not cong for these properties, so arguably, the design is OK as is, but at the same time... ugh.
TODO:
Recent work in
Algebrawrt 'sub'algebras (#2852 , #2854 , #2855 , #2859 , #2863 ...) exposes that, at least forAlgebra.Morphism.MagmaMonomorphism, certain properties make spurious appeal to the underlyingisMagmaproperty (which exposes∙-cong), when no appeal is made to∙-cong... so the dependency in the anonymous module is bogus.Fixing this in any sensible way, however, will be a
breakingchange, unless we regard this as abugfix?UPDATED: ugh. We need
setoid, but notcongfor these properties, so arguably, the design is OK as is, but at the same time... ugh.TODO:
Algebra.Morphism.MagmaMonomorphism:comm,sel,idem,cancelAlgebra.Morphism.GroupMonomorphism:⁻¹-congAlgebra.Module.Morphism.*Monomorphismas a consequence.