Lemma commrig_equiv_iso_is_equiv (X Y : ob commrig_category) : isweq (commrig_equiv_iso X Y). Proof. use isweq_iso. - exact (commrig_iso_equiv X Y). - intros y. use rigiso_paths. use subtypePath. + intros x0. use isapropisweq. + apply idpath. - intros x. use z_iso_eq. 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.