proposition: Lemma local_opcleaving_to_local_iso_cleaving_right_inv : γ •• δ = transportb (λ z, gg ==>[ z ] gg) (vcomp_linv α) (disp_id2 gg).
proof: Proof. unfold δ, local_opcleaving_to_local_iso_cleaving_disp_iso_cell. rewrite is_opcartesian_2cell_comm. unfold transportb. 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