proposition: Lemma pb_1cell_on_id_homot : cell_to_pb_obj_homot k₁ k₂.
proof: Proof. unfold cell_to_pb_obj_homot, k₁, k₂. rewrite <- !rwhisker_vcomp. rewrite !vassocl. pose (pb_on_1cell_cell f (linvunitor_invertible_2cell g)) as p. cbn in p. rewrite p. rewrite !vassocl. refine (!_). etrans. { do 3 apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite vcomp_linv. rewrite id2_rwhisker. rewrite id2_left. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite lunitor_triangle. rewrite <- vcomp_lunitor. rewrite !vassocl. apply maponpaths. rewrite <- lunitor_triangle. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. do 2 apply maponpaths_2. rewrite lwhisker_hcomp. rewrite triangle_l_inv. rewrite <- rwhisker_hcomp. apply idpath. 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