{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {t : CategoryTheory.Bicategory.LeftLift f g} →
            (desc : (s : CategoryTheory.Bicategory.LeftLift f g) → t ⟶ s) →
              (∀ (s : CategoryTheory.Bicategory.LeftLift f g) (τ : t ⟶ s), τ = desc s) → t.IsKan