proposition: Lemma fld_equiv_is_z_iso (X Y : ob fld_category) (f : ringiso (X : fld) (Y : fld)) : @is_z_isomorphism fld_category X Y (ringfunconstr (pr2 f)).
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence