Definition strict_double_cat_id_right_square {C : category} {D : twosided_disp_cat C C} {I : hor_id D} {Cm : hor_comp D} (rp : strict_double_cat_id_right I Cm) : UU := ∏ (x₁ x₂ y₁ y₂ : C) (v₁ : x₁ --> x₂) (v₂ : y₁ --> y₂) (h : D x₁ y₁) (k : D x₂ y₂) (s : h -->[ v₁ ][ v₂ ] k), double_hor_comp_mor Cm s (double_id_mor I v₂) = transportb_hor_mor (rp _ _ h) (rp _ _ k) 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.