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. 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.
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.