Proposition comp_left_adjoint_axioms : left_adjoint_axioms comp_left_adjoint_data. Proof. split ; cbn. - unfold ηη, εε. rewrite <- !lwhisker_vcomp. rewrite <- !rwhisker_vcomp. rewrite linvunitor_assoc. rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_rwhisker_alt. rewrite !vassocl. apply idpath. } refine (_ @ id2_rwhisker _ _). rewrite <- trl₁. rewrite <- !rwhisker_vcomp. rewrite !vassocl. do 2 apply maponpaths. refine (_ @ id2_right _). rewrite <- lwhisker_id2. rewrite <- trl₂. rewrite <- !lwhisker_vcomp. rewrite <- runitor_triangle. etrans. { do 10 apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker_rassociator. apply idpath. } etrans. { do 9 apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker_rassociator. apply idpath. } etrans. { do 8 apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker_rassociator. rewrite !vassocl. apply maponpaths. rewrite !lwhisker_vcomp. apply idpath. } rewrite <- !lwhisker_vcomp. rewrite !vassocr. do 2 apply maponpaths_2. rewrite !vassocl. etrans. { do 6 apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocr. rewrite <- lwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocl. etrans. { do 5 apply maponpaths. rewrite !vassocr. rewrite <- rassociator_rassociator. apply idpath. } rewrite !vassocl. etrans. { do 4 apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite lassociator_rassociator. rewrite id2_rwhisker. rewrite id2_left. rewrite !vassocl. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite <- rwhisker_lwhisker_rassociator. rewrite !vassocl. apply maponpaths. rewrite !lwhisker_vcomp. apply maponpaths. rewrite <- !lwhisker_vcomp. etrans. { apply maponpaths. rewrite !vassocr. rewrite rassociator_rassociator. rewrite !vassocl. apply maponpaths. rewrite !lwhisker_vcomp. rewrite lwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocr. rewrite rwhisker_rwhisker_alt. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite vcomp_whisker. rewrite !vassocl. apply idpath. } rewrite <- !lwhisker_vcomp. rewrite !vassocr. do 2 apply maponpaths_2. rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. rewrite <- rassociator_rassociator. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite rwhisker_vcomp. rewrite <- rwhisker_lwhisker_rassociator. rewrite <- !rwhisker_vcomp. rewrite !vassocl. apply maponpaths. etrans. { do 2 apply maponpaths. rewrite !vassocr. rewrite !lwhisker_vcomp. rewrite <- rassociator_rassociator. rewrite !vassocl. rewrite !lwhisker_vcomp. rewrite !vassocr. rewrite rassociator_lassociator. rewrite id2_left. rewrite <- !lwhisker_vcomp. apply idpath. } etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_lwhisker_rassociator. rewrite !vassocl. apply idpath. } etrans. { rewrite !vassocr. rewrite rwhisker_vcomp. rewrite lwhisker_vcomp. rewrite <- linvunitor_assoc. rewrite <- rwhisker_lwhisker_rassociator. rewrite !vassocl. apply maponpaths. rewrite !lwhisker_vcomp. apply maponpaths. etrans. { apply maponpaths. rewrite <- lwhisker_vcomp. rewrite !vassocr. rewrite rwhisker_lwhisker_rassociator. apply idpath. } rewrite !vassocr. rewrite rwhisker_vcomp. rewrite lwhisker_hcomp. rewrite <- linvunitor_natural. apply idpath. } rewrite <- !lwhisker_vcomp. rewrite <- !rwhisker_vcomp. rewrite <- !lwhisker_vcomp. rewrite !vassocr. rewrite rwhisker_lwhisker_rassociator. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite lwhisker_vcomp. rewrite lunitor_V_id_is_left_unit_V_id. rewrite rwhisker_hcomp. rewrite <- triangle_r_inv. rewrite <- lwhisker_hcomp. rewrite !lwhisker_vcomp. rewrite linvunitor_lunitor. rewrite !lwhisker_id2. apply idpath. } rewrite id2_right. use vcomp_move_L_Mp ; [ is_iso | ]. cbn. rewrite lunitor_lwhisker. apply idpath. - unfold εε, ηη. rewrite <- !lwhisker_vcomp. rewrite <- !rwhisker_vcomp. rewrite !vassocl. rewrite <- rinvunitor_triangle. rewrite !vassocl. etrans. { apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker. rewrite !vassocl. apply idpath. } refine (_ @ lwhisker_id2 _ _). rewrite <- trr₁. rewrite <- !lwhisker_vcomp. rewrite !vassocl. do 2 apply maponpaths. refine (_ @ id2_right _). rewrite <- id2_rwhisker. rewrite <- trr₂. rewrite <- !rwhisker_vcomp. rewrite <- lunitor_triangle. rewrite !vassocl. etrans. { do 9 apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_rwhisker. apply idpath. } rewrite !vassocr. rewrite <- rwhisker_rwhisker. apply idpath. } rewrite !vassocr. do 2 apply maponpaths_2. rewrite !vassocl. etrans. { rewrite !vassocr. rewrite <- lwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- lwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- lassociator_lassociator. rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite rwhisker_vcomp. rewrite lassociator_rassociator. rewrite id2_rwhisker. rewrite id2_left. apply idpath. } rewrite !vassocl. etrans. { do 5 apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. apply maponpaths. rewrite rwhisker_rwhisker. rewrite !vassocr. rewrite <- rwhisker_lwhisker. rewrite !vassocl. rewrite <- lassociator_lassociator. apply idpath. } rewrite !vassocr. apply maponpaths_2. rewrite !lwhisker_vcomp. rewrite !vassocl. use vcomp_move_R_Mp ; [ is_iso | ]. cbn. rewrite !vassocl. rewrite <- rwhisker_lwhisker_rassociator. refine (!_). etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_hcomp. rewrite <- triangle_r_inv. rewrite <- lwhisker_hcomp. apply idpath. } rewrite !lwhisker_vcomp. apply maponpaths. etrans. { rewrite !vassocl. do 2 apply maponpaths. rewrite !vassocr. rewrite lunitor_linvunitor. apply id2_left. } refine (!_). rewrite <- !lwhisker_vcomp. rewrite !vassocl. etrans. { do 3 apply maponpaths. rewrite !vassocr. rewrite lassociator_lassociator. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite !lwhisker_vcomp. rewrite lwhisker_lwhisker. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite rwhisker_rwhisker. rewrite !vassocl. apply idpath. } rewrite !vassocr. rewrite <- vcomp_whisker. rewrite !vassocl. apply maponpaths. etrans. { apply maponpaths. rewrite !vassocr. rewrite lunitor_triangle. apply idpath. } rewrite !vassocr. rewrite vcomp_lunitor. rewrite !vassocl. rewrite rassociator_lassociator. rewrite id2_right. rewrite !vassocr. rewrite lunitor_linvunitor. apply id2_left. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Section FromCompCartesian. End FromCompCartesian.