Definition idbinopfun_remove_right (A B : setwithbinop) (f : binopfun A B) : binopfuncomp f (idbinopfun B) = f. Proof. unfold binopfuncomp. unfold idbinopfun. use total2_paths_f. cbn. apply idpath. apply proofirrelevance. 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.