`(f : A -> B) : BiInv f -> IsEquiv f. Proof. intros [[g s] [h r]]. exact (isequiv_adjointify f g (fun x => ap f (ap g (r x)^ @ s (h x)) @ r x) s). Defined.
Require Import Basics Types.Prod Types.Equiv.