proposition: Lemma isrinvertibleisob {X Y : setwithbinop} (f : binopiso X Y) (x : X) (is : isrinvertible (@op Y) (f x)) : isrinvertible (@op X) x.
proof: Proof. unfold islinvertible. apply (twooutof3a (λ x0 : X, op x0 x) f). - assert (h : homot (funcomp f (λ y0 : Y, op y0 (f x))) (funcomp (λ x0 : X, op x0 x) f)). { intro x0; simpl. apply (pathsinv0 ((pr2 f) x0 x)). } apply (isweqhomot _ _ h). apply (pr2 (weqcomp f (make_weq _ is))). - apply (pr2 (pr1 f)). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions