{C : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} C} →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        {inst_1 : outParam ((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 : outParam (D → D → Type u_4)} →
                  {CD : outParam (D → Type w)} →
                    {inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))} →
                      {inst_5 : CategoryTheory.ConcreteCategory D FD} →
                        {P : Sort u} →
                          {forget₂ : CategoryTheory.Functor C D} →
                            {forget_comp :
                                autoParam (forget₂.comp (CategoryTheory.forget D) = CategoryTheory.forget C)
                                  CategoryTheory.HasForget₂.forget_comp._autoParam} →
                              {forget₂' : CategoryTheory.Functor C D} →
                                {forget_comp' :
                                    autoParam (forget₂'.comp (CategoryTheory.forget D) = CategoryTheory.forget C)
                                      CategoryTheory.HasForget₂.forget_comp._autoParam} →
                                  { forget₂ := forget₂, forget_comp := forget_comp } =
                                      { forget₂ := forget₂', forget_comp := forget_comp' } →
                                    (forget₂ ≍ forget₂' → P) → P