Definition oplax_slice_invertible_2cell_is_cartesian_1cell {c₁ c₂ : B} {s : c₁ --> c₂} {t₁ : oplax_slice_disp_bicat B a c₁} {t₂ : oplax_slice_disp_bicat B a c₂} (ss : t₁ -->[ s ] t₂) (Hss : is_invertible_2cell ss) : cartesian_1cell (oplax_slice_disp_bicat B a) ss. Proof. split. - intros c₃ t₃ s' ss'. simple refine (_ ,, _). + exact ((s' ◃ Hss^-1) • lassociator _ _ _ • ss'). + simple refine (_ ,, _). * abstract (cbn ; rewrite id2_rwhisker, id2_left ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite lwhisker_vcomp ; rewrite vcomp_rinv ; rewrite lwhisker_id2 ; rewrite id2_left ; rewrite !vassocr ; rewrite rassociator_lassociator ; rewrite id2_left ; apply idpath). * apply oplax_slice_disp_locally_groupoid. - cbn. intros c₃ t₃ s₁ s₂ α αα β ββ Lh Lh' ; cbn in *. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply (oplax_slice_disp_bicat B a) | ] ; apply cellset_property). + cbn. simple refine (_ ,, _). * abstract (pose (pr12 Lh) as p ; cbn in p ; rewrite id2_rwhisker in p ; rewrite id2_left in p ; pose (pr12 Lh') as p' ; cbn in p' ; rewrite id2_rwhisker in p' ; rewrite id2_left in p' ; cbn ; use (vcomp_lcancel (s₁ ◃ ss)) ; [ is_iso ; apply Hss | ] ; use (vcomp_lcancel (rassociator _ _ _)) ; [ is_iso | ] ; rewrite !vassocr ; refine (_ @ p) ; refine (_ @ ββ) ; refine (_ @ maponpaths (λ z, _ • z) (!p')) ; rewrite !vassocr ; apply maponpaths_2 ; rewrite rwhisker_rwhisker_alt ; rewrite !vassocl ; rewrite vcomp_whisker ; apply idpath). * apply cellset_property. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. 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.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. 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.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.LaxSlice. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Slice.