∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {l : b ⟶ c} {r : c ⟶ b}
  (adj : CategoryTheory.Bicategory.Adjunction l r) {g : a ⟶ b} {h : a ⟶ c},
  adj.homEquiv₂ =
    {
      toFun := fun α =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft g adj.unit)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator g l r).inv
              (CategoryTheory.Bicategory.whiskerRight α r))),
      invFun := fun γ =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight γ l)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator h r l).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft h adj.counit)
              (CategoryTheory.Bicategory.rightUnitor h).hom)),
      left_inv := ⋯, right_inv := ⋯ }