Definition slice_is_cartesian_1cell {c₁ c₂ : B} {s : c₁ --> c₂} {t₁ : slice_disp_bicat a c₁} {t₂ : slice_disp_bicat a c₂} (ss : t₁ -->[ s ] t₂) : cartesian_1cell (slice_disp_bicat a) ss. Proof. split. - intros c₃ t₃ s' ss'. simple refine (_ ,, _). + exact (comp_of_invertible_2cell ss' (comp_of_invertible_2cell (rassociator_invertible_2cell _ _ _) (lwhisker_of_invertible_2cell _ (inv_of_invertible_2cell ss)))). + simple refine (_ ,, _). * abstract (cbn ; rewrite id2_rwhisker ; rewrite id2_right ; rewrite !vassocl ; refine (_ @ id2_right _) ; apply maponpaths ; rewrite (maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite lwhisker_vcomp ; rewrite vcomp_linv ; rewrite lwhisker_id2 ; rewrite id2_left ; apply rassociator_lassociator). * apply disp_locally_groupoid_slice_disp_bicat. - cbn. intros c₃ t₃ s₁ s₂ α αα β ββ Lh Lh' ; cbn in *. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply (slice_disp_bicat a) | ] ; apply cellset_property). + cbn. simple refine (_ ,, _). * abstract (pose (pr12 Lh') as p ; cbn in p ; rewrite id2_rwhisker in p ; rewrite id2_right in p ; use (vcomp_rcancel (s₂ ◃ ss)) ; [ is_iso ; apply ss | ] ; use (vcomp_rcancel (lassociator _ _ _)) ; [ is_iso | ] ; rewrite !vassocl ; refine (_ @ !p) ; clear p ; pose (pr12 Lh) as p ; refine (_ @ ββ) ; cbn in p ; rewrite id2_rwhisker in p ; rewrite id2_right in p ; refine (_ @ maponpaths (λ z, z • _) p) ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; rewrite vcomp_whisker ; rewrite !vassocl ; rewrite rwhisker_rwhisker ; 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.