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