proposition: Proposition idtoiso_twosided_disp_concat_disp_path_idpath {C₁ C₂ : setcategory} {D : strict_twosided_disp_cat C₁ C₂} {x : C₁} {y : C₂} (xy : D x y) : idtoiso_twosided_disp_concat_disp_path (rx := idpath x) (rx' := idpath x) (ry := idpath y) (ry' := idpath y) (idpath xy) (idpath xy) = idpath xy.
proof: Proof. apply is_strict_strict_twosided_disp_cat. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness