proposition: Lemma istwobinopfuncomp {X Y Z : setwith2binop} (f : twobinopfun X Y) (g : twobinopfun Y Z) : istwobinopfun (funcomp (pr1 f) (pr1 g)).
proof: 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. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions