Lemma transport_of_left_partial_bifunctor_map_is_pointwise {F0 G0 : ob C -> ob C -> ob C} (F1 : ∏ x y1 y2 : ob C, C⟦y1,y2⟧ -> C⟦F0 x y1, F0 x y2⟧) (gamma : F0 = G0) {y1 y2 : ob C} (x : C) (g : C⟦y1,y2⟧) : transportf (fun T : C -> C -> C => ∏ a b1 b2 : C, C⟦b1,b2⟧ -> C⟦T a b1, T a b2⟧) gamma F1 x y1 y2 g = double_transport (toforallpaths (λ _ : ob C, C) (F0 x) (G0 x) (toforallpaths (λ _ : ob C, C -> C) F0 G0 gamma x) y1) (toforallpaths (λ _ : ob C, C) (F0 x) (G0 x) (toforallpaths (λ _ : ob C, C -> C) F0 G0 gamma x) y2) (F1 x y1 y2 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.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import BifunctorNotations.