fact: Definition twobinopmonocomp {X Y Z : setwith2binop} (f : twobinopmono X Y) (g : twobinopmono Y Z) : twobinopmono X Z := make_twobinopmono (inclcomp (pr1 f) (pr1 g)) (istwobinopfuncomp f g).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions