fact: Definition transportb_twosided_disp_functor {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 g' : y₁ --> y₂} (q : g = g') (fg : xy₁ -->[ f' ][ g' ] xy₂) : #2 FG (transportb_disp_mor2 p q fg) = transportb_disp_mor2 (maponpaths (λ z, #F z) p) (maponpaths (λ z, #G z) q) (#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