Definition disp_adj_equiv_between_cartesian_1cell_inv : r ;; l ==>[ lunitor _ ] id_disp _ := w₁. Let ζ : r ;; l ==>[ lunitor _ ] id_disp _ := disp_adj_equiv_between_cartesian_1cell_inv. Local Definition help_cell₂ : gg₁ ==>[ linvunitor (id₁ x) ▹ f] gg₂. Proof. refine (transportf (λ z, _ ==>[ z ] _) _ (γ₁ •• disp_inv_cell γ₂)). abstract (cbn ; rewrite !vassocr ; rewrite lunitor_linvunitor ; rewrite id2_left ; rewrite rwhisker_hcomp ; rewrite lunitor_V_id_is_left_unit_V_id ; rewrite <- triangle_l_inv ; rewrite <- lwhisker_hcomp ; apply maponpaths_2 ; rewrite linvunitor_assoc ; rewrite lwhisker_hcomp ; rewrite triangle_r_inv ; rewrite <- rwhisker_hcomp ; rewrite lunitor_V_id_is_left_unit_V_id ; apply idpath). Defined.
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.CategoryTheory.DisplayedCats.Examples.Opposite. 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.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.TransportLaws. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.StrictPseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.StrictToPseudo. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Projection. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Section MapAndCellFromCartesians. End MapAndCellFromCartesians.