Lemma transport_of_bifunctor_map_is_pointwise {C : univalent_category} {F0 G0 : ob C -> ob C -> ob C} (F1 : ∏ x1 x2 y1 y2 : ob C, C⟦x1,x2⟧ -> C⟦y1,y2⟧ -> C⟦F0 x1 y1, F0 x2 y2⟧) (gamma : F0 = G0) {x1 x2 y1 y2 : ob C} (f : C⟦x1,x2⟧) (g : C⟦y1,y2⟧) : transportf (fun T : C -> C -> C => ∏ a1 a2 b1 b2 : C, C⟦a1,a2⟧ -> C⟦b1,b2⟧ -> C⟦T a1 b1, T a2 b2⟧) gamma F1 x1 x2 y1 y2 f g = double_transport (toforallpaths (λ _ : ob C, C) (F0 x1) (G0 x1) (toforallpaths (λ _ : ob C, C -> C) F0 G0 gamma x1) y1) (toforallpaths (λ _ : ob C, C) (F0 x2) (G0 x2) (toforallpaths (λ _ : ob C, C -> C) F0 G0 gamma x2) y2) (F1 _ _ _ _ f g). Proof. induction gamma. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import TensorNotation. Import TensorNotation.