Definition commring_precategory_data : precategory_data := make_precategory_data commring_precategory_ob_mor (λ (X : commring), (rigisotorigfun (idrigiso X))) (fun (X Y Z : commring) (f : ringfun X Y) (g : ringfun Y Z) => rigfuncomp f g). Local Lemma commring_id_left (X Y : commring) (f : ringfun X Y) : rigfuncomp (rigisotorigfun (idrigiso X)) f = f. Proof. use rigfun_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.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.