`{Funext} X Y (f : X -> Y) `{IsEquiv _ _ f} : ismono f. 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.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.