proposition: Lemma negate_mon_unit : - mon_unit = mon_unit.
proof: Proof. change ((fun x => - mon_unit = x) mon_unit). apply (transport _ (left_inverse mon_unit)). apply symmetry, right_identity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra