proposition: Lemma islcancelablemonob {X Y : setwithbinop} (f : binopmono X Y) (x : X) (is : islcancelable (@op Y) (f x)) : islcancelable (@op X) x.
proof: Proof. unfold islcancelable. apply (isincltwooutof3a (λ x0 : X, op x x0) f (pr2 (pr1 f))). assert (h : homot (funcomp f (λ y0 : Y, op (f x) y0)) (funcomp (λ x0 : X, op x x0) f)). { intro x0; simpl. apply (pathsinv0 ((pr2 f) x x0)). } apply (isinclhomot _ _ h). apply (isinclcomp f (make_incl _ is)). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions