proposition: Lemma local_opcleaving_to_local_iso_cleaving_left_inv : δ •• γ = transportb (λ z, ff ==>[ z ] ff) (vcomp_rinv α) (disp_id2 ff).
proof: Proof. unfold δ, local_opcleaving_to_local_iso_cleaving_disp_iso_cell. use (is_opcartesian_2cell_unique _ Hγ). - refine (transportf (λ z, _ ==>[ z ] _) _ γ). abstract (rewrite vcomp_rinv ; rewrite id2_right ; apply idpath). - rewrite disp_vassocr. rewrite is_opcartesian_2cell_comm. rewrite disp_mor_transportf_postwhisker. rewrite disp_id2_left. unfold transportb. rewrite !transport_f_f. apply maponpaths_2. apply cellset_property. - unfold transportb. rewrite disp_mor_transportf_prewhisker. rewrite disp_id2_right. unfold transportb. rewrite transport_f_f. apply maponpaths_2. apply cellset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.TransportLaws UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispInvertibles