proposition: Proposition is_cat_iso_to_is_z_isomorphism_inv_laws : is_functor is_cat_iso_to_is_z_isomorphism_inv_data.
proof: Proof. split. - intro x ; cbn -[catiso_inv_mor]. use catiso_inv_mor_eq ; cbn -[catiso_inv_mor]. rewrite functor_id. rewrite id_right. refine (!_). etrans. { refine (!_). apply (pr1_idtoiso_concat (!(catiso_catiso_inv_ob F_iso x))). } rewrite pathsinv0l. apply idpath. - intros x y z f g ; cbn -[catiso_inv_mor]. use catiso_inv_mor_eq ; cbn -[catiso_inv_mor]. rewrite functor_comp. rewrite !(catiso_catiso_inv_mor F_iso). refine (!_). etrans. { rewrite !assoc. etrans. { do 6 apply maponpaths_2. refine (!_). apply (pr1_idtoiso_concat (!(catiso_catiso_inv_ob F_iso x))). } rewrite pathsinv0l. cbn. rewrite id_left. rewrite !assoc'. apply maponpaths. rewrite !assoc. etrans. { do 3 apply maponpaths_2. refine (!_). apply (pr1_idtoiso_concat (!(catiso_catiso_inv_ob F_iso y))). } rewrite pathsinv0l. cbn. rewrite id_left. rewrite !assoc'. apply maponpaths. etrans. { refine (!_). apply (pr1_idtoiso_concat (!(catiso_catiso_inv_ob F_iso z))). } rewrite pathsinv0l. apply idpath. } cbn. rewrite id_right. 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