proposition: 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) (funcomp (invmap (pr1 f)) (funcomp invx (pr1 f))).
proof: 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). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions