{A B : Type} `{IsHSet B} (m : A -> B) : IsInjective m -> IsEmbedding m. Proof. intros isi b. apply hprop_allpath; intros [x p] [y q]. apply path_sigma_hprop; simpl. exact (isi x y (p @ q^)). Defined.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.