fact: Definition isabgropisob {X Y : setwithbinop} (f : binopiso X Y) (is : isabgrop (@op Y)) : isabgrop (@op X) := tpair _ (isgropisob f is) (iscommisob f (commax_is is)).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions