{X Y} (f : X -> Y) (s : forall x1 x2, (f x1 = f x2) -> (x1 = x2)) (H : forall x1 x2, (@ap X Y f x1 x2) o (s x1 x2) == idmap) : IsEmbedding f. Proof. intros y. apply hprop_allpath. intros [x1 p1] [x2 p2]. apply path_sigma with (s x1 x2 (p1 @ p2^)). abstract (rewrite transport_paths_Fl; cbn; rewrite (H x1 x2 (p1 @ p2^)); rewrite inv_pp, inv_V; apply concat_pV_p). Defined.
Require Import HoTT.Basics HoTT.Types.