Lemma pb_1cell_on_comp_homot : cell_to_pb_obj_homot k₁ k₂. Proof. unfold cell_to_pb_obj_homot, k₁, k₂. rewrite <- !rwhisker_vcomp. rewrite (pb_on_1cell_cell f γ). rewrite !vassocr. do 2 apply maponpaths_2. rewrite !vassocl. refine (!_). etrans. { do 5 apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite !vassocl. apply idpath. } etrans. { do 4 apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite vcomp_linv. rewrite id2_rwhisker. rewrite id2_left. rewrite !vassocl. apply idpath. } use (vcomp_lcancel (lassociator _ _ _)) ; [ is_iso | ]. rewrite !vassocr. rewrite <- lwhisker_lwhisker. rewrite <- lassociator_lassociator. rewrite (pb_on_1cell_cell f β). rewrite <- !lwhisker_vcomp. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite lassociator_rassociator. rewrite id2_rwhisker. rewrite id2_left. rewrite !vassocl. apply idpath. } refine (!_). etrans. { do 6 apply maponpaths. rewrite !vassocr. rewrite <- lassociator_lassociator. do 4 apply maponpaths_2. rewrite !vassocl. rewrite rwhisker_vcomp. rewrite lassociator_rassociator. rewrite id2_rwhisker. rewrite id2_right. apply idpath. } etrans. { do 5 apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite rassociator_lassociator. rewrite lwhisker_id2. rewrite id2_left. rewrite !vassocl. apply idpath. } etrans. { do 4 apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite lwhisker_vcomp. rewrite vcomp_linv. rewrite lwhisker_id2. rewrite id2_rwhisker. rewrite id2_left. rewrite !vassocl. apply idpath. } etrans. { do 3 apply maponpaths. rewrite !vassocr. rewrite lassociator_lassociator. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply idpath. } refine (!_). etrans. { rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. apply idpath. } apply maponpaths. cbn. rewrite <- !lwhisker_vcomp. rewrite !vassocr. do 2 (use vcomp_move_R_Mp ; [ is_iso | ] ; cbn). rewrite !vassocl. refine (!_). etrans. { do 4 apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite rassociator_rassociator. apply idpath. } rewrite !vassocr. rewrite lassociator_rassociator. apply id2_left. } etrans. { apply maponpaths. rewrite !vassocr. rewrite lwhisker_lwhisker. rewrite !vassocl. apply idpath. } etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite <- vcomp_whisker. rewrite !vassocl. rewrite <- lwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite (pb_on_1cell_cell f α). rewrite !vassocl. do 3 apply maponpaths. refine (_ @ id2_right _). apply maponpaths. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. apply idpath. } etrans. { apply maponpaths. rewrite vassocr. rewrite rwhisker_vcomp. rewrite vcomp_linv. rewrite id2_rwhisker. apply id2_left. } apply lassociator_rassociator. 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.