Lemma unique_internal_adjoint_equivalence {C : bicat} {X Y : C} (l : C⟦X,Y⟧) (HC : is_univalent_2_1 C) (A₁ : left_adjoint_equivalence l) (A₂ : left_adjoint_equivalence l) : A₁ = A₂. Proof. use subtypePath. - intro x. apply isapropdirprod. + apply isapropdirprod ; apply C. + apply isapropdirprod ; apply isaprop_is_invertible_2cell. - cbn. use total2_paths_f. + apply (isotoid_2_1 HC). refine (adjoint_unique_map l A₁ A₂ ,, _). exact (adjoint_unique_map_iso l A₁ A₂). + rewrite transportf_dirprod. apply dirprod_paths. * rewrite transport_two_cell_FlFr. rewrite !maponpaths_for_constant_function ; cbn. rewrite id2_left. rewrite <- idtoiso_2_1_lwhisker. unfold isotoid_2_1. pose (homotweqinvweq (idtoiso_2_1 _ _,, HC Y X (left_adjoint_right_adjoint A₁) (left_adjoint_right_adjoint A₂))) as p. cbn in p. rewrite p ; clear p. cbn. exact (transport_unit l A₁ A₂). * cbn. rewrite transport_two_cell_FlFr. rewrite !maponpaths_for_constant_function ; cbn. rewrite id2_right. use vcomp_move_R_pM. { is_iso. } cbn. rewrite <- idtoiso_2_1_rwhisker. unfold isotoid_2_1. pose (homotweqinvweq (idtoiso_2_1 _ _,, HC Y X (left_adjoint_right_adjoint A₁) (left_adjoint_right_adjoint A₂))) as p. cbn in p. rewrite p ; clear p. cbn. symmetry. exact (transport_counit l A₁ A₂). 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.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.TransportLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv.