Proposition idtoiso_twosided_disp_concat {C₁ C₂ : category} {D : twosided_disp_cat C₁ C₂} {x : C₁} {y : C₂} {xy₁ xy₂ xy₃ : D x y} (p : xy₁ = xy₂) (q : xy₂ = xy₃) : pr1 (idtoiso_twosided_disp (idpath x) (idpath y) p) ;;2 pr1 (idtoiso_twosided_disp (idpath x) (idpath y) q) = transportb_disp_mor2 (id_left _) (id_left _) (pr1 (idtoiso_twosided_disp (idpath x) (idpath y) (p @ q))). Proof. induction p, q ; cbn. rewrite id_two_disp_left. 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.