`{IsMonoid A} (a x y : A) {p : x * a = mon_unit} {q : a * y = mon_unit} : x = y. Proof. refine ((right_identity x)^ @ ap _ q^ @ _). refine (associativity _ _ _ @ _). refine (ap (fun x => x * y) p @ _). apply left_identity. Defined.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.