Definition rig_precategory_data : precategory_data := make_precategory_data rig_precategory_ob_mor (λ (X : rig), (rigisotorigfun (idrigiso X))) (fun (X Y Z : rig) (f : rigfun X Y) (g : rigfun Y Z) => rigfuncomp f g). Local Definition rig_id_left (X Y : rig) (f : rigfun 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.