Proposition is_cat_iso_to_is_z_isomorphism_laws : @is_inverse_in_precat cat_of_setcategory C D F is_cat_iso_to_is_z_isomorphism_inv. Proof. split. - use functor_eq ; [ apply homset_property | ]. use functor_data_eq_alt. + intros x ; cbn. apply homotinvweqweq. + intros x y f ; cbn -[catiso_inv_mor]. rewrite (catiso_inv_mor_cat_iso F_iso). rewrite !assoc'. apply maponpaths. refine (_ @ id_right _). apply maponpaths. etrans. { refine (!_). apply (pr1_idtoiso_concat (!(catiso_inv_ob_catiso F_iso y))). } rewrite pathsinv0l. apply idpath. - use functor_eq ; [ apply homset_property | ]. use functor_data_eq_alt. + intros x ; cbn. exact (homotweqinvweq (catiso_ob_weq F_iso) x). + intros x y f ; cbn -[catiso_inv_mor]. rewrite (catiso_catiso_inv_mor F_iso). rewrite !assoc'. apply maponpaths. refine (_ @ id_right _). apply maponpaths. etrans. { refine (!_). apply (pr1_idtoiso_concat (!(catiso_catiso_inv_ob F_iso y))). } rewrite pathsinv0l. apply idpath. Qed.
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.