{X : Type u_3} →
  [inst : TopologicalSpace X] →
    {motive : IrreducibleSpace X → Sort u} →
      ([toPreirreducibleSpace : PreirreducibleSpace X] → (toNonempty : Nonempty X) → motive ⋯) →
        (t : IrreducibleSpace X) → motive t