Proposition idtoiso_twosided_disp_concat_strict_base_path {C : setcategory} {x : C} (rx rx' : x = x) : idtoiso rx · idtoiso rx' = identity _. 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.
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.