Definition binopfuncomp_assoc (A B C D : setwithbinop) (f : binopfun A B) (g : binopfun B C) (h : binopfun C D) : binopfuncomp (binopfuncomp f g) h = binopfuncomp f (binopfuncomp g h). Proof. unfold binopfuncomp. apply maponpaths. apply isapropisbinopfun. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors.