proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.catiso UniMath.CategoryTheory.CategoryEquality