Lemma rig_iso_equiv (X Y : ob rig_category) : z_iso X Y -> rigiso (X : rig) (Y : rig). Proof. intro f. use make_rigiso. - exact (make_weq (pr1 (pr1 f)) (rig_iso_is_equiv X Y f)). - exact (pr2 (pr1 f)). 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.