fact: Definition left_adjoint_axioms {a b : B} {f : a --> b} (αd : left_adjoint_data f) : UU := let g := left_adjoint_right_adjoint αd in let η := left_adjoint_unit αd in let ε := left_adjoint_counit αd in linvunitor f • (η ▹ f) • rassociator _ _ _ • (f ◃ ε) • runitor f = id2 f × rinvunitor g • (g ◃ η) • lassociator _ _ _ • (ε ▹ g) • lunitor g = id2 g.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells