Lemma istwobinopfuncomp {X Y Z : setwith2binop} (f : twobinopfun X Y) (g : twobinopfun Y Z) : istwobinopfun (pr1 g ∘ pr1 f). Proof. set (ax1f := pr1 (pr2 f)). set (ax2f := pr2 (pr2 f)). set (ax1g := pr1 (pr2 g)). set (ax2g := pr2 (pr2 g)). split. - intros a b. simpl. rewrite (ax1f a b). rewrite (ax1g (pr1 f a) (pr1 f b)). apply idpath. - intros a b. simpl. rewrite (ax2f a b). rewrite (ax2g (pr1 f a) (pr1 f b)). apply idpath. Qed.