Definition hor_trans_id_right_sq {C : predoublecategory_sq_hor_data} { a b c d : C } {f: a -h-> b} {g: a -v-> c} {h: b -v-> d} {k: c -h-> d} (α : sqq f g h k) : sqq (f ·h (hor_identity b)) g h (k ·h (hor_identity d)) := boundary_sq_transport (id_hor_right f) (id_hor_right k) α.
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.