Definition internal_right_adj_axioms {a b : B} {g : b --> a} (αd : internal_right_adj_data g) : UU := let f := internal_right_adj_left_adjoint αd in let η := internal_right_adj_unit αd in let ε := internal_right_adj_counit αd in linvunitor f • (η ▹ f) • rassociator _ _ _ • (f ◃ ε) • runitor f = id2 f × rinvunitor g • (g ◃ η) • lassociator _ _ _ • (ε ▹ g) • lunitor g = id2 g.
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.