Lemma istwobinopfuninvmap {X Y : setwith2binop} (f : twobinopiso X Y) : istwobinopfun (invmap (pr1 f)). Proof. set (ax1f := pr1 (pr2 f)). set (ax2f := pr2 (pr2 f)). split. - intros a b. apply (invmaponpathsweq (pr1 f)). rewrite (homotweqinvweq (pr1 f) (op1 a b)). rewrite (ax1f (invmap (pr1 f) a) (invmap (pr1 f) b)). rewrite (homotweqinvweq (pr1 f) a). rewrite (homotweqinvweq (pr1 f) b). apply idpath. - intros a b. apply (invmaponpathsweq (pr1 f)). rewrite (homotweqinvweq (pr1 f) (op2 a b)). rewrite (ax2f (invmap (pr1 f) a) (invmap (pr1 f) b)). rewrite (homotweqinvweq (pr1 f) a). rewrite (homotweqinvweq (pr1 f) b). apply idpath. Qed.