26 Dec
2020
26 Dec
'20
2:54 p.m.
Koji Miyazato wrote:
You can use `MonoidNull`. from monoid-subclasses to avoid an `Eq` constraint.
For groups, there is no difference between `MonoidNull` and `Eq`, as you can define `x == y` be `null (x <> inv y)`. There are monoids which `==` is not even decidable but `null` is (e.g. context-free grammars with equality defined by the language it defines), but such monoid necessarily has no `Group` instance.
A beautiful example of topological groups: Their topology is completely determined by the neighbourhoods of the identity element. If the identity element is isolated, the entire group is discrete. Olaf