Lemma isbinopfuncomp {X Y Z : setwithbinop} (f : binopfun X Y) (g : binopfun Y Z) : isbinopfun (g ∘ f). Proof. set (axf := binopfunisbinopfun f). set (axg := binopfunisbinopfun g). intros a b. simpl. rewrite (axf a b). rewrite (axg (f a) (f b)). apply idpath. Qed.