Definition setwith2binop_precategory_data : precategory_data := make_precategory_data setwith2binop_precategory_ob_mor (λ (X : setwith2binop), ((idtwobinopiso X) : twobinopfun X X)) (fun (X Y Z : setwith2binop) (f : twobinopfun X Y) (g : twobinopfun Y Z) => twobinopfuncomp f g). Local Lemma setwith2binop_id_left (X Y : setwith2binop) (f : twobinopfun X Y) : twobinopfuncomp (idtwobinopiso X) f = f. Proof. use twobinopfun_paths. use idpath. 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.