{motive : CompactlyGenerated → Sort u_1} →
  (t : CompactlyGenerated) →
    ((toTop : TopCat) →
        [is_compactly_generated : UCompactlyGeneratedSpace ↑toTop] →
          motive { toTop := toTop, is_compactly_generated := is_compactly_generated }) →
      motive t