proposition: Lemma isotoid_functorcat_pointwise_aux (C : precategory_data) (D : category) (H : is_univalent D) (F G : ob [C, D, D]) (p: F = G) (c: C) : let α := idtoiso p in toforallpaths (fun _ : ob C => ob D) (pr1 (pr1 F)) (pr1 (pr1 G)) (maponpaths pr1 (maponpaths pr1 (isotoid (functor_category C D) (is_univalent_functor_category C D H) α))) c = isotoid D H (functor_z_iso_pointwise_if_z_iso C D D F G α (pr2 α) c).
proof: Proof. induction p. cbn delta in *. unfold functor_z_iso_pointwise_if_z_iso. rewrite isotoid_idtoiso. unfold idtoiso. simpl. apply idtoiso_inj; try assumption. rewrite idtoiso_isotoid. simpl. apply z_iso_eq. apply idpath. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core