{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : C → C → Type u_2} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {D : Type u_3} →
              [inst_3 : CategoryTheory.Category.{v_2, u_3} D] →
                {FD : D → D → Type u_4} →
                  {CD : D → Type w} →
                    [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                      [inst_5 : CategoryTheory.ConcreteCategory D FD] →
                        {motive : CategoryTheory.HasForget₂ C D → Sort u} →
                          ((forget₂ : CategoryTheory.Functor C D) →
                              (forget_comp : forget₂.comp (CategoryTheory.forget D) = CategoryTheory.forget C) →
                                motive { forget₂ := forget₂, forget_comp := forget_comp }) →
                            (t : CategoryTheory.HasForget₂ C D) → motive t