{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {u : b ⟶ a} →
        (t : CategoryTheory.Bicategory.LeftLift u (CategoryTheory.CategoryStruct.id a)) →
          t.IsAbsKan → CategoryTheory.Bicategory.Adjunction t.lift u