Lemma pb_1cell_on_id_homot : cell_to_pb_obj_homot k₁ k₂. 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.
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.