Definition ring_precategory_data : precategory_data := make_precategory_data ring_precategory_ob_mor (λ (X : ring), (rigisotorigfun (idrigiso X))) (fun (X Y Z : ring) (f : ringfun X Y) (g : ringfun Y Z) => rigfuncomp f g). Local Lemma ring_id_left (X Y : ring) (f : ringfun 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.