Lemma transport_of_functor_map_is_pointwise (C : precategory_data) (D : precategory) (F0 G0 : ob C -> ob D) (F1 : ∏ a b : ob C, a --> b -> F0 a --> F0 b) (gamma : F0 = G0 ) (a b : ob C) (f : a --> b) : transportf (fun x : ob C -> ob D => ∏ a0 b0 : ob C, a0 --> b0 -> x a0 --> x b0) gamma F1 a b f = double_transport (toforallpaths (λ _ : ob C, D) F0 G0 gamma a) (toforallpaths (λ _ : ob C, D) F0 G0 gamma b) (F1 a b f). Proof. induction gamma. apply idpath. 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.