Lemma J_2_0_comp {a : B} : J_2_0 (internal_adjoint_equivalence_identity a) = r a. Proof. unfold J_2_0. refine (! (!_ @ _)). + exact (J'_2_0_transport _ _ (isotoid_2_0_idtoiso_2_0 HB (idpath a))). + rewrite (functtransportf (idtoiso_2_0 a a) (Y a a)). apply maponpaths_2. exact (homotweqinvweqweq (make_weq (idtoiso_2_0 a a) (HB a a)) (idpath a)). 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.