Definition pb_reflect_iso_help : is_invertible_2cell (α ▹ p₁). Proof. apply (Hf z (h₁ · p₁) (h₂ · p₁) (α ▹ p₁)). use eq_is_invertible_2cell. - exact (rassociator _ _ _ • (_ ◃ γ) • lassociator _ _ _ • ((α ▹ p₂) ▹ g) • rassociator _ _ _ • (_ ◃ γ^-1) • lassociator _ _ _). - abstract (rewrite !vassocl ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite rwhisker_rwhisker ; rewrite !vassocr ; apply maponpaths_2 ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite vcomp_whisker ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; rewrite rwhisker_rwhisker ; rewrite !vassocl ; rewrite lassociator_rassociator ; apply id2_right). - use is_invertible_2cell_vcomp ; [ | is_iso ]. use is_invertible_2cell_vcomp ; [ | is_iso ; apply property_from_invertible_2cell ]. use is_invertible_2cell_vcomp ; [ | is_iso ]. use is_invertible_2cell_vcomp. + is_iso. apply property_from_invertible_2cell . + apply is_invertible_2cell_rwhisker. exact Hα. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Morphisms.Properties.Composition. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Examples.OpCellBicatLimits. Section FromPBCartesian. End FromPBCartesian.