Lemma rig_iso_equiv_is_equiv (X Y : rig_category) : isweq (rig_iso_equiv X Y). Proof. use isweq_iso. - exact (rig_equiv_z_iso X Y). - intros x. use z_iso_eq. use rigfun_paths. use idpath. - intros y. use rigiso_paths. use subtypePath. + intros x0. use isapropisweq. + 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.