proposition: 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: Proof. induction gamma. apply idpath. 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