Definition help_pred_mor_pb_on_1cell : pb_ump_mor (mirror_has_pb_ump (pb_obj_has_pb_ump f (pr12 g₂))) (make_pb_cone (f /≃ pr12 g₁) ((π₂ : B ⟦ f /≃ pr12 g₁, pr1 g₁ ⟧) · pr1 α) (π₁ · id₁ b₁) γ) ==> f /≃₁ pr22 α. Proof. use pb_ump_cell. - apply (mirror_has_pb_ump (pb_obj_has_pb_ump f (pr12 g₂))). - exact (pb_ump_mor_pr2 (pb_obj_has_pb_ump f (pr12 g₂)) (mirror_cone (make_pb_cone (f /≃ pr12 g₁) (π₂ · pr1 α) (π₁ · id₁ b₁) γ)) • (pb_on_1cell_pr2 _ _)^-1). - exact (pb_ump_mor_pr1 (pb_obj_has_pb_ump f (pr12 g₂)) (mirror_cone (make_pb_cone (f /≃ pr12 g₁) (π₂ · pr1 α) (π₁ · id₁ b₁) γ)) • runitor _ • (pb_on_1cell_pr1 _ _)^-1). - abstract (cbn ; rewrite <- !rwhisker_vcomp ; rewrite !vassocl ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; refine (!_) ; etrans ; [ apply maponpaths_2 ; exact (pb_ump_mor_cell (pb_obj_has_pb_ump f (pr12 g₂)) (mirror_cone (make_pb_cone (f /≃ pr12 g₁) (π₂ · pr1 α) (π₁ · id₁ b₁) γ))) | ] ; rewrite !vassocl ; apply maponpaths ; etrans ; [ do 3 apply maponpaths ; rewrite !vassocr ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite !vassocl ; apply idpath | ] ; etrans ; [ do 2 apply maponpaths ; rewrite !vassocr ; rewrite rwhisker_vcomp ; rewrite vcomp_linv ; rewrite id2_rwhisker ; rewrite id2_left ; rewrite !vassocl ; apply idpath | ] ; rewrite !vassocr ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite pb_on_1cell_cell ; rewrite !vassocl ; refine (!_) ; etrans ; [ do 3 apply maponpaths ; rewrite !vassocr ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite !vassocl ; apply idpath | ] ; etrans ; [ do 2 apply maponpaths ; rewrite !vassocr ; rewrite rwhisker_vcomp ; rewrite vcomp_linv ; rewrite id2_rwhisker ; rewrite id2_left ; rewrite !vassocl ; apply idpath | ]; apply idpath). 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.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.PullbackFunctions. Require Import UniMath.Bicategories.Limits.Examples.OpCellBicatLimits. Import PullbackFunctions.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Slice. Require Import UniMath.Bicategories.Logic.DisplayMapBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatSlice.