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