proposition: Proposition idtoiso_twosided_disp_concat_strict_base_path {C : setcategory} {x : C} (rx rx' : x = x) : idtoiso rx · idtoiso rx' = identity _.
proof: Proof. assert (rx = idpath _) as s. { apply isaset_ob. } rewrite s ; clear s. assert (rx' = idpath _) as s. { apply isaset_ob. } rewrite s ; clear s. apply id_left. 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