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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core.