Lemma local_cleaving_to_local_iso_cleaving_disp_left_inv : γ •• δ = transportb (λ z, ff ==>[ z ] ff) (vcomp_rinv α) (disp_id2 ff). Proof. unfold δ, local_cleaving_to_local_iso_cleaving_disp_inv. use (is_cartesian_2cell_unique _ Hγ). - refine (transportf (λ z, _ ==>[ z ] _) _ γ). abstract (rewrite vcomp_rinv ; rewrite id2_left ; apply idpath). - rewrite disp_vassocl. rewrite is_cartesian_2cell_comm. rewrite disp_mor_transportf_prewhisker. rewrite disp_id2_right. unfold transportb. rewrite !transport_f_f. apply maponpaths_2. apply cellset_property. - unfold transportb. rewrite disp_mor_transportf_postwhisker. rewrite disp_id2_left. unfold transportb. rewrite transport_f_f. apply maponpaths_2. apply cellset_property. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.TransportLaws. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles.