proposition: Lemma isinj_embedding {A B : Type} (m : A -> B) : IsEmbedding m -> isinj m.
proof: Proof. intros ise x y p. pose (ise (m y)). assert (q : (x;p) = (y;1) :> hfiber m (m y)) by apply path_ishprop. exact (ap pr1 q). Defined.
imports: Basics Types.Sigma Types.Forall Types.Paths Types.Unit Types.Arrow