(3/6) ... there is a *formal space* of functions ℕ → 𝑋. This space has as its points the functions ℕ → 𝑋, whatever they might be. But a formal space is much more than its collection of points, and is in particular not defined by this collection. Unlike its collection of points, the formal space of functions itself does not depend on foundational assumptions. It is a very concrete and entirely combinatorial gadget.

We should not require that the collection of functions ℕ → 𝑋 is literally the union over its subsets { 𝑓 | 𝑓(𝑖) = 𝑓(𝑗) } (indexed by pairs (𝑖,𝑗) such that 𝑖 < 𝑗), as the definition of streamlessness does.

Instead we should ask that the formal space of functions ℕ → 𝑋 is the join over its open subspaces ⟨ 𝑓 | 𝑓(𝑖) = 𝑓(𝑗) ⟩. A set is *Noetherian* iff this holds. This condition might sound abstract and involved, but it boils down to a straightforward condition involving dialogues (https://iblech.gitlab.io/streamless-sets/Scratch.Mathstodon.html).

For a set 𝑋 to be Noetherian, every *black box* 𝑓 : ℕ → 𝑋, which we can only query (for given input receive output), must have duplicate values. If a set is Noetherian, not only does every actual function 𝑓 : ℕ → 𝑋 have duplicate values, but also every function-like gadget which we cannot realize as an actual function because the law of excluded middle or some generic filter is missing.

Unlike streamlessness, which is more an assertion about the available functions than it is a statement about the set in question, and easily breaks under universe extension, the Noetherian condition really is only about the set.

And indeed: The cartesian product of Noetherian sets is Noetherian, independently of foundational assumptions.

But there is no reason to expect this for streamlessness.