(2/6) On first sight, the definition of streamlessness looks like a clean ∀∃ condition. No pesky negations in sight, unlike for instance in the constructively problematic saying "a function is injective if it maps nonequal inputs to nonequal outputs".

But the universal quantifier references the totality of functions ℕ → 𝑋. This totality is vastly underspecified: Does it only contain the computable functions? Computable relative to some oracle? Can dependent choice, or even the law of excluded middle, be used to construct functions? Are we secretly living in a forcing extension containing many more functions than the base universe, such as Cohen's model where there are more than ℵ₁ many functions ℕ → 𝟚?

A classical reference proof for the product of two streamless sets 𝑋 and 𝑌 being streamless runs like this: Let 𝑓 : ℕ → 𝑋 × 𝑌. Write 𝑓(𝑛) = (𝑔(𝑛), ℎ(𝑛)). By a combinatorial Ramsey-style argument involving the law of excluded middle and making use of streamlessness of 𝑋, there is a strongly monotonically increasing function 𝑝 : ℕ → ℕ such that 𝑔 ∘ 𝑝 : ℕ → 𝑋 is constant. (Consider the set { 𝑖 ∈ ℕ | ¬∃𝑗 > 𝑖. 𝑓(𝑖) = 𝑓(𝑗) }. If it is finite, set 𝑝(0) to be an upper bound. If it is infinite, extract a stream without duplicates.) By streamlessness of 𝑌, the stream ℎ ∘ 𝑝 contains duplicates at some positions 𝑖 < 𝑗. So ℎ(𝑝(𝑖)) = ℎ(𝑝(𝑗)), and also 𝑔(𝑝(𝑖)) = 𝑔(𝑝(𝑗)).)

Without the law of excluded middle, the function 𝑝 is only a partial function and hence we cannot apply streamlessness of 𝑌 to ℎ ∘ 𝑝. The classical proof doesn't carry over to the constructive setting.

Now formal topology teaches us that ...