Definition left_adjoint_equivalence_eq_to_pb {B : bicat} {b₁ b₂ b₃ : B} {f : b₁ --> b₃} {g : b₂ --> b₃} (cone₁ cone₂ : pb_cone f g) (H₂ : has_pb_ump cone₂) (p : pr1 cone₁ = pr1 cone₂) (qp1 : invertible_2cell (idtoiso_2_0 _ _ (!p) · pb_cone_pr1 cone₁) (pb_cone_pr1 cone₂)) (qp2 : invertible_2cell (idtoiso_2_0 _ _ (!p) · pb_cone_pr2 cone₁) (pb_cone_pr2 cone₂)) (path : (qp1^-1 ▹ f) • rassociator _ _ _ • (_ ◃ pb_cone_cell cone₁) • lassociator _ _ _ • (qp2 ▹ g) = pr1 (pb_cone_cell cone₂)) : has_pb_ump cone₁. Proof. induction cone₁ as [ q cone ]. induction cone as [ qp₁ cone ]. induction cone as [ qp₂ γ ]. induction cone₂ as [ q' cone ]. induction cone as [ qp₁' cone ]. induction cone as [ qp₂' γ' ]. cbn in *. induction p ; cbn in *. use (id_left_adjoint_equivalence_to_pb _ _ H₂). - exact (comp_of_invertible_2cell (linvunitor_invertible_2cell _) qp1). - exact (comp_of_invertible_2cell (linvunitor_invertible_2cell _) qp2). - abstract (cbn ; use vcomp_move_L_pM ; [ is_iso ; apply property_from_invertible_2cell | ] ; cbn ; refine (_ @ path) ; rewrite <- !rwhisker_vcomp ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; apply maponpaths_2 ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite !vassocl ; rewrite lunitor_triangle ; rewrite vcomp_lunitor ; rewrite !vassocr ; apply maponpaths_2 ; rewrite <- lunitor_triangle ; rewrite !vassocr ; rewrite rassociator_lassociator ; rewrite id2_left ; 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.