fact: Definition twobinopisocomp {X Y Z : setwith2binop} (f : twobinopiso X Y) (g : twobinopiso Y Z) : twobinopiso X Z := make_twobinopiso (weqcomp (pr1 f) (pr1 g)) (istwobinopfuncomp f g).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions