Definition J_2_1_comp {a b : B} {f : a --> b} : J_2_1 (id2_invertible_2cell f) = r a b f. Proof. unfold J_2_1. refine (! (!_ @ _)). + exact (J'_2_1_transport _ _ (isotoid_2_1_idtoiso_2_1 HB (idpath f))). + rewrite (functtransportf (idtoiso_2_1 f f) (Y a b f f)). apply maponpaths_2. exact (homotweqinvweqweq (make_weq (idtoiso_2_1 f f) (HB _ _ f f)) (idpath f)). Qed. End J21. Section J20. Context {B : bicat}. Variable (HB : is_univalent_2_0 B) (Y : ∏ (a b : B), adjoint_equivalence a b → UU) (r : ∏ (a : B), Y _ _ (internal_adjoint_equivalence_identity a)). Local Definition Y'_2_0 : ∏ {a b : B}, a = b → UU := λ a b p, Y a b (idtoiso_2_0 a b p). Local Definition J'_2_0 {a b : B} (p : a = b) : Y'_2_0 p. Proof. induction p. exact (r a). Defined.
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.