proposition: Lemma is_internal_adjunction_identity (a : C) : left_adjoint_axioms (internal_adjunction_data_identity a).
proof: Proof. split. - etrans. { apply maponpaths_2. etrans; [apply (!vassocr _ _ _) | ]. etrans. { apply maponpaths. etrans; [apply lunitor_lwhisker | ]. apply maponpaths, pathsinv0, lunitor_runitor_identity. } etrans; [apply (!vassocr _ _ _) | ]. etrans. { apply maponpaths. etrans; [apply rwhisker_vcomp | ]. etrans; [apply maponpaths, linvunitor_lunitor | ]. apply id2_rwhisker. } apply id2_right. } etrans; [apply maponpaths, pathsinv0, lunitor_runitor_identity | ]. apply linvunitor_lunitor. - etrans. { apply maponpaths_2. etrans; [apply (!vassocr _ _ _) | ]. etrans. { apply maponpaths. etrans. { apply maponpaths. apply maponpaths. apply lunitor_runitor_identity. } apply runitor_rwhisker. } etrans; [apply (!vassocr _ _ _) | ]. apply maponpaths. etrans; [ apply lwhisker_vcomp | ]. apply maponpaths. apply linvunitor_lunitor. } etrans; [apply (!vassocr _ _ _) | ]. etrans. { apply maponpaths. etrans; [apply maponpaths_2, lwhisker_id2 | ]. apply id2_left. } etrans; [apply maponpaths, lunitor_runitor_identity | ]. apply rinvunitor_runitor. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Groupoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Isos UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.BicategoryLaws