proposition: Lemma functor_eq_from_functor_z_iso_idtoiso (C : precategory_data) (D : category) (H : is_univalent D) (F G : ob [C, D, D]) (p : F = G) : functor_eq_from_functor_z_iso H F G (idtoiso p) = p.
proof: Proof. simpl; apply functor_eq_eq_from_functor_ob_eq. apply D. unfold functor_eq_from_functor_z_iso. unfold functor_eq. rewrite base_total2_paths. unfold pr1_functor_eq_from_functor_z_iso. rewrite base_total2_paths. unfold pr1_pr1_functor_eq_from_functor_iso. apply (invmaponpathsweq (weqtoforallpaths _ _ _ )). simpl. rewrite toforallpaths_funextsec. apply funextsec; intro a. rewrite idtoiso_functorcat_compute_pointwise. apply isotoid_idtoiso. Qed.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence