proposition: Lemma unary_idempotency `{UnaryIdempotent A f} x : f (f x) = f x.
proof: Proof. change (f (f x)) with (Compose f f x). apply (ap (fun g => g x)). change (Compose f f = f). apply idempotency. apply _. Qed.
imports: HoTT.Basics HoTT.Types HoTT.Truncations.Core