Lemma isbinopfuninvmap {X Y : setwithbinop} (f : binopiso X Y) : isbinopfun (invmap (pr1 f)). Proof. set (axf := pr2 f). intros a b. apply (invmaponpathsweq (pr1 f)). rewrite (homotweqinvweq (pr1 f) (op a b)). rewrite (axf (invmap (pr1 f) a) (invmap (pr1 f) b)). rewrite (homotweqinvweq (pr1 f) a). rewrite (homotweqinvweq (pr1 f) b). apply idpath. Qed.