Definition isrinvertibleisof {X Y : setwithbinop} (f : binopiso X Y) (x : X) (is : isrinvertible (@op X) x) : isrinvertible (@op Y) (f x). Proof. unfold isrinvertible. apply (twooutof3b f). - apply (pr2 (pr1 f)). - assert (h : homot (f ∘ (λ x0 : X, op x0 x)) (λ x0 : X, op (f x0) (f x))). { intro x0; simpl. apply (pr2 f x0 x). } apply (isweqhomot _ _ h). apply (pr2 (weqcomp (make_weq _ is) f)). Defined.