Definition trivial_cartesian_2cell_is_invertible {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_cartesian_2cell (trivial_displayed_bicat B₁ B₂) β) : is_invertible_2cell β. Proof. cbn in *. unfold is_cartesian_2cell in Hβ. pose (Hβ f₁ g₂ (id2 _) (id2 _)) as lift. pose (inv := iscontrpr1 lift). cbn in lift, inv. use make_is_invertible_2cell. - exact (pr1 inv). - abstract (pose (Hβ f₁ g₁ (id2 _) β) as m ; cbn in m ; pose (proofirrelevance _ (isapropifcontr m)) as i ; simple refine (maponpaths pr1 (i (β • pr1 inv ,, _) (id₂ g₁ ,, _))) ; cbn ; [ cbn ; rewrite vassocl ; rewrite (pr2 inv) ; apply id2_right | apply id2_left ]). - abstract (exact (pr2 inv)). 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.