Lemma is_internal_adjunction_identity (a : C) : left_adjoint_axioms (internal_adjunction_data_identity a). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.BicategoryLaws.