`{Funext} {X Y} (f : X -> Y) : IsInjective f -> ismono f. Proof. intros ? ? ? ? H'. apply path_forall. apply ap10 in H'. hnf in *. eauto. Qed.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.