proposition: Lemma ismono_isequiv `{Funext} X Y (f : X -> Y) `{IsEquiv _ _ f} : ismono f.
proof: Proof. intros ? g h H'. apply ap10 in H'. apply path_forall. intro x. transitivity (f^-1 (f (g x))). - by rewrite eissect. - transitivity (f^-1 (f (h x))). * apply ap. apply H'. * by rewrite eissect. Qed.
imports: Basics Types.Sigma Types.Forall Types.Paths Types.Unit Types.Arrow