proposition: Lemma independent_transportation_commutes {C : univalent_category} {F G : C -> C -> C} {x1 x2 y1 y2 : C} (p1 : F x1 y1 = G x1 y1) (p2 : F x2 y2 = G x2 y2) (f : C⟦F x1 y1, F x2 y2⟧) : transportf (λ c : C, C ⟦ G x1 y1, c ⟧) p2 (transportf (λ c : C, C ⟦ c, F x2 y2 ⟧) p1 f) = transportf (λ c : C, C ⟦ c, G x2 y2 ⟧) p1 (transportf (λ c : C, C ⟦ F x1 y1, c ⟧) p2 f).
proof: Proof. induction p1 ; induction p2. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.Core.Univalence UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories