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