Lemma pb_on_2cell_homot : cell_to_pb_obj_homot k₁ k₂. Proof. unfold cell_to_pb_obj_homot, k₁, k₂. rewrite pb_on_1cell_cell. rewrite <- !rwhisker_vcomp. rewrite !vassocl. do 2 apply maponpaths. etrans. { do 3 apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite rwhisker_vcomp. rewrite vcomp_linv. rewrite id2_rwhisker. rewrite id2_left. apply idpath. } rewrite !vassocl. rewrite pb_on_1cell_cell. rewrite !vassocl. refine (!_). etrans. { apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite rwhisker_vcomp. rewrite vcomp_linv. rewrite id2_rwhisker. rewrite id2_left. rewrite !vassocl. apply maponpaths. rewrite !vassocr. do 2 apply maponpaths_2. rewrite !vassocl. rewrite <- rwhisker_lwhisker. rewrite !vassocr. apply maponpaths_2. rewrite lwhisker_vcomp. apply maponpaths. exact (!p). 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.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Limits.Pullbacks.