Proposition is_cat_iso_to_is_z_isomorphism_inv_laws : is_functor is_cat_iso_to_is_z_isomorphism_inv_data. 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.
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.