proposition: Proposition idtoiso_twosided_disp_concat_disp_path {C₁ C₂ : setcategory} {D : strict_twosided_disp_cat C₁ C₂} {x : C₁} {rx rx' : x = x} {y : C₂} {ry ry' : y = y} {xy₁ xy₂ xy₃ : D x y} (p : transportf (λ z, D z y) rx (transportf (λ z, D x z) ry xy₁) = xy₂) (q : transportf (λ z, D z y) rx' (transportf (λ z, D x z) ry' xy₂) = xy₃) : xy₁ = xy₃.
proof: Proof. assert (rx = idpath _) as s. { apply isaset_ob. } rewrite s in p ; clear s. assert (rx' = idpath _) as s. { apply isaset_ob. } rewrite s in q ; clear s. assert (ry = idpath _) as s. { apply isaset_ob. } rewrite s in p ; clear s. assert (ry' = idpath _) as s. { apply isaset_ob. } rewrite s in q ; clear s. cbn in p, q ; cbn. rewrite p, q. apply idpath. 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