fact: Definition twobinopfuncomp {X Y Z : setwith2binop} (f : twobinopfun X Y) (g : twobinopfun Y Z) : twobinopfun X Z := make_twobinopfun (funcomp (pr1 f) (pr1 g)) (istwobinopfuncomp f g).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions