Definition is_cat_iso_to_is_z_isomorphism_inv_data : functor_data D C. Proof. use make_functor_data. - exact (catiso_inv_ob F_iso). - exact (λ x y f, catiso_inv_mor F_iso f). 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.