fact: Definition transportb_twosided_disp_functor_left {C₁ C₁' C₂ C₂' : category} {F : C₁ ⟶ C₁'} {G : C₂ ⟶ C₂'} {D₁ : twosided_disp_cat C₁ C₂} {D₂ : twosided_disp_cat C₁' C₂'} (FG : twosided_disp_functor F G D₁ D₂) {x₁ x₂ : C₁} {y₁ y₂ : C₂} {xy₁ : D₁ x₁ y₁} {xy₂ : D₁ x₂ y₂} {f f' : x₁ --> x₂} (p : f = f') {g : y₁ --> y₂} (fg : xy₁ -->[ f' ][ g ] xy₂) : #2 FG (transportb (λ z, xy₁ -->[ z ][ g ] xy₂) p fg) = transportb (λ z, FG _ _ xy₁ -->[ z ][ _ ] FG _ _ xy₂) (maponpaths (λ z, #F z) p) (#2 FG fg).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete UniMath.CategoryTheory.TwoSidedDisplayedCats.Total