Definition id_left_adjoint_equivalence_to_pb_ump_1 : pb_ump_1 (make_pb_cone q qpr1 qpr2 qγ). Proof. intro qc. use make_pb_1cell. - exact (pb_ump_mor H₂ qc). - exact (comp_of_invertible_2cell (lwhisker_of_invertible_2cell _ lpr1) (pb_ump_mor_pr1 H₂ qc)). - exact (comp_of_invertible_2cell (lwhisker_of_invertible_2cell _ lpr2) (pb_ump_mor_pr2 H₂ qc)). - abstract (cbn ; use (vcomp_rcancel (_ ◃ (lpr2 ▹ g))) ; [ is_iso ; apply property_from_invertible_2cell | ] ; rewrite lwhisker_vcomp ; rewrite lc ; rewrite <- lwhisker_vcomp ; refine (maponpaths (λ z, _ • z) (pb_ump_mor_cell H₂ qc) @ _) ; cbn ; rewrite !vassocr ; rewrite rwhisker_lwhisker ; rewrite !vassocl ; apply maponpaths ; rewrite <- rwhisker_vcomp ; rewrite !vassocl ; do 3 apply maponpaths ; rewrite rwhisker_lwhisker_rassociator ; rewrite !vassocr ; apply maponpaths_2 ; rewrite rwhisker_vcomp ; rewrite !vassocl ; rewrite lwhisker_vcomp ; rewrite vcomp_linv ; rewrite lwhisker_id2 ; rewrite id2_right ; apply idpath). 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.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.TransportLaws. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles. Require Import UniMath.Bicategories.Limits.Pullbacks.