proposition: Proposition idtoiso_disp_cartesian_lift {C : category} (D : disp_cat C) (HD : cleaving D) {x y : C} {f g : x --> y} (yy : D y) (p : g = f) : (idtoiso_disp (idpath _) (maponpaths (λ (h : x --> y), pr1 (HD _ _ h _)) p) ;; HD y x f yy = transportf (λ z, _ -->[ z ] _) (p @ !(id_left _)) (HD y x g yy))%mor_disp.
proof: Proof. induction p ; cbn. rewrite id_left_disp. apply idpath. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Presheaf UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Examples.Opposite