Proposition idtoiso_twosided_disp_concat_strict {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₃) : pr1 (idtoiso_twosided_disp rx ry p) ;;2 pr1 (idtoiso_twosided_disp rx' ry' q) = transportb_disp_mor2 (idtoiso_twosided_disp_concat_strict_base_path rx rx') (idtoiso_twosided_disp_concat_strict_base_path ry ry') (idtoiso_twosided_disp (idpath _) (idpath _) (idtoiso_twosided_disp_concat_disp_path p q)). Proof. induction p, q. assert (rx = idpath _) as s. { apply isaset_ob. } rewrite s ; clear s. assert (rx' = idpath _) as s. { apply isaset_ob. } rewrite s ; clear s. assert (ry = idpath _) as s. { apply isaset_ob. } rewrite s ; clear s. assert (ry' = idpath _) as s. { apply isaset_ob. } rewrite s ; clear s. rewrite idtoiso_twosided_disp_concat_disp_path_idpath. clear rx rx' ry ry'. cbn. rewrite (id_two_disp_left (D := D)). use transportb_disp_mor2_eq. 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.