fact: Definition transportf_hor_comp_data_path {C : category} {D : twosided_disp_cat C C} {ψ₁ ψ₂ : ∏ (x y z : C), D x y → D y z → D x z} (p : ψ₁ = ψ₂) {x y z : C} (h : D x y) (k : D y z) : ψ₁ x y z h k = ψ₂ x y z h k := toforallpaths _ _ _ (toforallpaths _ _ _ (toforallpaths _ _ _ (toforallpaths _ _ _ (toforallpaths _ _ _ p x) y) z) h) k.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Categories.CategoryOfSetCategories UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.StrictTwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics