{A B} (e f : A <~> B) : e oE f^-1 = 1 -> e = f. Proof. intro h. refine ((ecompose_eV_e _ _)^ @ ap (fun ef => ef oE f) h @ ecompose_1e _). Defined.
Require Import Basics.Overture Basics.Equivalences Types.Equiv.