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