{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {F : C → D} →
          {P : Sort u} →
            {map : {X Y : C} → (X ⟶ Y) → (F X ⟶ F Y)} →
              {map_id :
                  autoParam
                    (∀ {X : C}, map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (F X))
                    CategoryTheory.Functorial.map_id._autoParam} →
                {map_comp :
                    autoParam
                      (∀ {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
                        map (CategoryTheory.CategoryStruct.comp f g) =
                          CategoryTheory.CategoryStruct.comp (map f) (map g))
                      CategoryTheory.Functorial.map_comp._autoParam} →
                  {map' : {X Y : C} → (X ⟶ Y) → (F X ⟶ F Y)} →
                    {map_id' :
                        autoParam
                          (∀ {X : C},
                            map' (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (F X))
                          CategoryTheory.Functorial.map_id._autoParam} →
                      {map_comp' :
                          autoParam
                            (∀ {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
                              map' (CategoryTheory.CategoryStruct.comp f g) =
                                CategoryTheory.CategoryStruct.comp (map' f) (map' g))
                            CategoryTheory.Functorial.map_comp._autoParam} →
                        { map := map, map_id := map_id, map_comp := map_comp } =
                            { map := map', map_id := map_id', map_comp := map_comp' } →
                          (map ≍ map' → P) → P