Definition comp_essentially_surj_is_inv2cell {h₁ : slice_bicat b₁} {h₂ : slice_bicat b₂} (α : h₁ --> pb_psfunctor B f h₂) : is_invertible_2cell (comp_essentially_surj_cell_slice α). Proof. use is_invertible_2cell_in_slice_bicat. cbn. use is_invertible_2cell_pb_ump_cell. - unfold comp_essentially_surj_cell_pr1. is_iso. + apply property_from_invertible_2cell. + apply property_from_invertible_2cell. + apply property_from_invertible_2cell. - unfold comp_essentially_surj_cell_pr2. is_iso. + apply property_from_invertible_2cell. + apply property_from_invertible_2cell. 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.Bicategories.Core.Bicat. Import Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Slice. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.UniversalArrow. Require Import UniMath.Bicategories.PseudoFunctors.Examples.PullbackFunctor. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.PullbackFunctions. Import PullbackFunctions.Notations.