Lemma ring_equiv_is_z_iso (X Y : ob ring_category) (f : ringiso (X : ring) (Y : ring)) : @is_z_isomorphism ring_category X Y (ringfunconstr (pr2 f)). Proof. exists (ringfunconstr (pr2 (invrigiso f))). use make_is_inverse_in_precat. - use rigfun_paths. use funextfun. intros x. use homotinvweqweq. - use rigfun_paths. use funextfun. intros y. use homotweqinvweq. 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.