Definition pr1_functor_eq_from_functor_z_iso (C : precategory_data) (D : category) (H : is_univalent D) (F G : ob [C , D, D]) : z_iso F G -> pr1 F = pr1 G. Proof. intro A. apply (total2_paths_f (pr1_pr1_functor_eq_from_functor_iso C D H F G A)). unfold pr1_pr1_functor_eq_from_functor_iso. apply funextsec; intro a. apply funextsec; intro b. apply funextsec; intro f. rewrite transport_of_functor_map_is_pointwise. rewrite toforallpaths_funextsec. etrans. { apply double_transport_idtoiso. } rewrite idtoiso_isotoid. rewrite idtoiso_isotoid. etrans. { rewrite <- assoc. apply cancel_precomposition. apply (nat_trans_ax (pr1 A)). } etrans. { apply cancel_postcomposition. apply nat_trans_inv_pointwise_inv_after_p_z_iso. } rewrite assoc. apply remove_id_left; try apply idpath. set (TA' := z_iso_after_z_iso_inv A). set (TA'' := nat_trans_comp_pointwise _ _ _ _ _ _ _ _ _ TA'). apply TA''. Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence.