fact: Definition binopfuncomp {X Y Z : setwithbinop} (f : binopfun X Y) (g : binopfun Y Z) : binopfun X Z := make_binopfun (funcomp (pr1 f) (pr1 g)) (isbinopfuncomp f g).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions