Lemma isInjective_inl {A B : UU} : isInjective (@inl A B). Proof. intros ? ?. refine (isweqinvmap (@paths_inl_inl_equiv _ _ _ _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.