Definition commrig_precategory_data : precategory_data := make_precategory_data commrig_precategory_ob_mor (λ (X : commrig), (rigisotorigfun (idrigiso X))) (fun (X Y Z : commrig) (f : rigfun X Y) (g : rigfun Y Z) => rigfuncomp f g). Local Lemma commrig_id_left (X Y : commrig) (f : rigfun X Y) : rigfuncomp (rigisotorigfun (idrigiso X)) f = f. Proof. use rigfun_paths. apply 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.Algebra.Monoids. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence.