Lemma isinvisof {X Y : setwithbinop} (f : binopiso X Y) (unx : X) (invx : X → X) (is : isinv (@op X) unx invx) : isinv (@op Y) (pr1 f unx) ((pr1 f) ∘ invx ∘ invmap (pr1 f)). Proof. set (axf := pr2 f). set (axinvf := pr2 (invbinopiso f)). simpl in axf, axinvf. split. - intro a. apply (invmaponpathsweq (pr1 (invbinopiso f))). simpl. rewrite (axinvf ((pr1 f) (invx (invmap (pr1 f) a))) a). rewrite (homotinvweqweq (pr1 f) unx). rewrite (homotinvweqweq (pr1 f) (invx (invmap (pr1 f) a))). apply (pr1 is). - intro a. apply (invmaponpathsweq (pr1 (invbinopiso f))). simpl. rewrite (axinvf a ((pr1 f) (invx (invmap (pr1 f) a)))). rewrite (homotinvweqweq (pr1 f) unx). rewrite (homotinvweqweq (pr1 f) (invx (invmap (pr1 f) a))). apply (pr2 is). Qed.