{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {l : b ⟶ c} →
        {r : c ⟶ b} →
          CategoryTheory.Bicategory.Adjunction l r →
            {g : a ⟶ b} →
              {h : a ⟶ c} → (CategoryTheory.CategoryStruct.comp g l ⟶ h) ≃ (g ⟶ CategoryTheory.CategoryStruct.comp h r)