search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.26k stars 193 forks source link

Improved notation for inverses and units in groups #1156

Open mikeshulman opened 4 years ago

mikeshulman commented 4 years ago

As discussed at #1155, it would be nice to be able to write something like x^-1 instead of - x for inverses in a multiplicative group (i.e. a group with mc_mult_scope opened). (There's probably no need to have anything similar for Mult instances, since those are generally used for rings and the multiplicative monoid of a ring is never nontrivially a group, instead we have Recip for inverting nonzero elements in fields.)

It would also be nice to be able to use 0 and 1 for the unit elements in additive and multiplicative monoids respectively.

Alizter commented 3 years ago

Would it be sensible to use x^ for inverses, since it is more economical to type. We can probably set this up without affecting our notation for paths.

mikeshulman commented 3 years ago

Perhaps.

(I think you mean "affecting".)