Definition boundary_sq_transport {C : predoublecategory_ob_mor_sq_data} { a b c d : C } {f1: a -h-> b} {g1: a -v-> c} {h1: b -v-> d} {k1: c -h-> d} {f2: a -h-> b} {k2: c -h-> d} (eqf: f1 = f2) (eqk: k1 = k2) (α : sqq f2 g1 h1 k2) : sqq f1 g1 h1 k1 := transportb (fun f0 => sqq f0 _ _ _) eqf (transportb (fun k0 => sqq _ _ _ k0) eqk α).
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.