Definition transportb_hor_mor {C : category} {D : twosided_disp_cat C C} {x₁ x₂ y₁ y₂ : C} {vx : x₁ --> x₂} {vy : y₁ --> y₂} {h₁ h₂ : D x₁ y₁} (p : h₁ = h₂) {k₁ k₂ : D x₂ y₂} (q : k₁ = k₂) (s : h₂ -->[ vx ][ vy ] k₂) : h₁ -->[ vx ][ vy ] k₁ := transportb (λ z, z -->[ _ ][ _ ] _) p (transportb (λ z, _ -->[ _ ][ _ ] z) q s).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics.