proposition: Lemma pb_on_2cell_homot : cell_to_pb_obj_homot k₁ k₂.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Limits.Pullbacks