Lemma is_invertible_2cell_pb_ump_cell_left : pb_ump_cell Hp φ ψ α β r • is_invertible_2cell_pb_ump_cell_inv = id₂ φ. Proof. use (pb_ump_eq Hp). - apply id2. - apply id2. - rewrite !id2_rwhisker, !id2_right. rewrite lassociator_rassociator, id2_left. rewrite vassocl. rewrite lassociator_rassociator. apply id2_right. - unfold is_invertible_2cell_pb_ump_cell_inv. rewrite <- rwhisker_vcomp. rewrite !pb_ump_cell_pr1. apply vcomp_rinv. - unfold is_invertible_2cell_pb_ump_cell_inv. rewrite <- rwhisker_vcomp. rewrite !pb_ump_cell_pr2. apply vcomp_rinv. - apply id2_rwhisker. - apply id2_rwhisker. Qed.
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.