Definition trivial_invertible_is_cartesian_2cell {x₁ x₂ : B₁} {y₁ : trivial_displayed_bicat B₁ B₂ x₁} {y₂ : trivial_displayed_bicat B₁ B₂ x₂} {f₁ f₂ : x₁ --> x₂} {g₁ : y₁ -->[ f₁ ] y₂} {g₂ : y₁ -->[ f₂ ] y₂} (α : f₁ ==> f₂) (β : g₁ ==>[ α ] g₂) (Hβ : is_invertible_2cell β) : is_cartesian_2cell (trivial_displayed_bicat B₁ B₂) β. Proof. intros h h' γ ββ ; cbn in *. use iscontraprop1. - abstract (use invproofirrelevance ; intros τ₁ τ₂ ; use subtypePath ; [ intro ; apply cellset_property | ] ; use (vcomp_rcancel _ Hβ) ; exact (pr2 τ₁ @ !(pr2 τ₂))). - refine (ββ • Hβ^-1 ,, _). 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.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.EquivToAdjequiv. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Properties. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. 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.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.Cartesians. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Trivial.