Definition locally_grpd_cartesian {B : bicat} (HB : locally_groupoid B) {e b : B} (p : e --> b) {x : B} {f g : x --> e} (γ : f ==> g) : is_cartesian_2cell_sfib p γ. Proof. intros h α δp q. pose (α_iso := make_invertible_2cell (HB _ _ _ _ α)). pose (γ_iso := make_invertible_2cell (HB _ _ _ _ γ)). use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ; use (vcomp_rcancel _ γ_iso) ; cbn ; exact (pr22 φ₁ @ !(pr22 φ₂))). - refine (α • γ_iso^-1 ,, _ ,, _). + abstract (rewrite <- rwhisker_vcomp ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite q ; apply idpath). + abstract (rewrite !vassocl ; rewrite vcomp_linv ; apply id2_right). 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.DisplayedCats.StreetFibration. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence.