Lemma isunitisof {X Y : setwithbinop} (f : binopiso X Y) (unx : X) (is : isunit (@op X) unx) : isunit (@op Y) (f unx). Proof. set (axf := pr2 f). split. - intro a. change (f unx) with (pr1 f unx). apply (invmaponpathsweq (pr1 (invbinopiso f))). rewrite (pr2 (invbinopiso f) (pr1 f unx) a). simpl. rewrite (homotinvweqweq (pr1 f) unx). apply (pr1 is). - intro a. change (f unx) with (pr1 f unx). apply (invmaponpathsweq (pr1 (invbinopiso f))). rewrite (pr2 (invbinopiso f) a (pr1 f unx)). simpl. rewrite (homotinvweqweq (pr1 f) unx). apply (pr2 is). Qed.