Definition transportf_set_rel {X₁ X₂ Y₁ Y₂ : UU} (R₁ : X₁ → Y₁ → hSet) (R₂ : X₂ → Y₂ → hSet) {f₁ f₂ : X₁ → X₂} (p : f₂ = f₁) {g₁ g₂ : Y₁ → Y₂} (q : g₂ = g₁) (α : ∏ (x : X₁) (y : Y₁), R₁ x y → R₂ (f₂ x) (g₂ y)) {a : X₁} {b : Y₁} (r : R₁ a b) : transportf (λ (h : X₁ → X₂), ∏ (x : X₁) (y : Y₁), R₁ x y → R₂ (h x) (g₁ y)) p (transportf (λ (h : Y₁ → Y₂), ∏ (x : X₁) (y : Y₁), R₁ x y → R₂ (f₂ x) (h y)) q α) a b r = transportf (λ z, R₂ z _) (eqtohomot p _) (transportf (λ z, R₂ _ z) (eqtohomot q _) (α a b r)).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedFibration.