fact: Definition make_isunit {X : UU} {opp : binop X} {un0 : X} (H1 : islunit opp un0) (H2 : isrunit opp un0) : isunit opp un0 := make_dirprod H1 H2.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions