{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {x : B} →
            (h : c ⟶ x) →
              CategoryTheory.Functor (CategoryTheory.Bicategory.LeftExtension f g)
                (CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g h))