Definition make_adjoint_equivalence {a b : B} (f : a --> b) (g : b --> a) (η : identity _ ==> g ∘ f) (ε : f ∘ g ==> identity _) (triangle1 : linvunitor f • (η ▹ f) • rassociator _ _ _ • (f ◃ ε) • runitor f = id2 f) (triangle2 : rinvunitor g • (g ◃ η) • lassociator _ _ _ • (ε ▹ g) • lunitor g = id2 g) (η_iso : is_invertible_2cell η) (ε_iso : is_invertible_2cell ε) : adjoint_equivalence a b := f ,, ((g ,, (η ,, ε)) ,, ((triangle1 ,, triangle2) ,, (η_iso ,, ε_iso))).
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.