{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (G : CategoryTheory.Functor C (Type w)) →
      CategoryTheory.Functor G.Elements (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat))