{C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.ObjectProperty C → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty D