{P : TopCat → Prop} →
  {P_1 : Sort u_1} →
    {toTop : TopCat} →
      {is_compact : CompactSpace ↑toTop} →
        {is_hausdorff : T2Space ↑toTop} →
          {prop : P toTop} →
            {toTop' : TopCat} →
              {is_compact' : CompactSpace ↑toTop'} →
                {is_hausdorff' : T2Space ↑toTop'} →
                  {prop' : P toTop'} →
                    { toTop := toTop, is_compact := is_compact, is_hausdorff := is_hausdorff, prop := prop } =
                        { toTop := toTop', is_compact := is_compact', is_hausdorff := is_hausdorff', prop := prop' } →
                      (toTop = toTop' → P_1) → P_1