proposition: Lemma isbinopfuncomp {X Y Z : setwithbinop} (f : binopfun X Y) (g : binopfun Y Z) : isbinopfun (funcomp (pr1 f) (pr1 g)).
proof: Proof. set (axf := pr2 f). set (axg := pr2 g). intros a b. simpl. rewrite (axf a b). rewrite (axg (pr1 f a) (pr1 f b)). apply idpath. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions