Proposition idtoiso_twosided_disp_triple_concat {C₁ C₂ : category} {D : strict_twosided_disp_cat C₁ C₂} {x x' : C₁} {f : x --> x'} {y y' : C₂} {g : y --> y'} {xy wxy : D x y} (p p' : wxy = xy) {xy' wxy' : D x' y'} (q q' : xy' = wxy') (fg : xy -->[ f ][ g ] xy') : idtoiso_twosided_disp (idpath x) (idpath y) p ;;2 fg ;;2 idtoiso_twosided_disp (idpath x') (idpath y') q = idtoiso_twosided_disp (idpath x) (idpath y) p' ;;2 fg ;;2 idtoiso_twosided_disp (idpath x') (idpath y') q'. Proof. assert (p = p') as s. { apply is_strict_strict_twosided_disp_cat. } rewrite s ; clear s. assert (q = q') as s. { apply is_strict_strict_twosided_disp_cat. } rewrite s ; clear s. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness.