Definition internal_right_adj_counit {a b : B} {g : b --> a} (αd : internal_right_adj_data g) : g · internal_right_adj_left_adjoint αd ==> identity b := pr22 αd.
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.Invertible_2cells.