Definition is_catiso_weq_is_z_isomorphism {C D : setcategory} (F : C ⟶ D) : is_catiso F ≃ @is_z_isomorphism cat_of_setcategory C D F. Proof. use weqimplimpl. - exact (is_cat_iso_to_is_z_isomorphism F). - exact (is_z_isomorphism_to_is_cat_iso F). - apply isaprop_is_catiso. - apply isaprop_is_z_isomorphism. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Section FromIso. End FromIso.