fact: Definition make_invstruct {X : UU} {opp : binop X} {is : ismonoidop opp} (inv0 : X -> X) (H : isinv opp (unel_is is) inv0) : invstruct opp is := tpair _ inv0 H.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions