Weeknotes 2025-W27 › Too cool to exist: an idea bites the dust [01C5]

I had a very “cool” idea last term for a version of synthetic domain theory that handles non-determinism with the same grace that ordinary synthetic domain theory handles recursion and continuity. The idea was to treat non-determinism as an orthogonality property, so that we would have special types in which you can take the “sum” of two elements, and these sums would automatically be preserved by all functions without any need to check anything, in the same way that you can take the limit of a chain in the synthetic way and then these are preserved automatically by every function.

To be precise, I had hoped to study the types that are orthogonal to the inclusion \(2\hookrightarrow T(2)\) where \(T\) is Hyland’s “co-partial map classifier”. I finally got around to looking into this idea this week.

Unfortunately, it will never work: in particular, the synthetic Sierpiński space \(\Sigma \) will pretty much never satisfy the orthogonality condition that I had in mind. In most cases, the Sierpiński space will be orthogonal to the comparison map \(2^\top \to T(2)\) where \(2^\top \) is the inverted Sierpiński cone of the discrete space \(2\); this would follow by dualising the results of my recent LICS paper, which hold so long as \(\Sigma \) is closed under finite disjunctions and satisfies Phoa’s principle. So in that case, we can consider just whether it is possible for \(\Sigma \) to be orthogonal to the canonical closed embedding \(2\hookrightarrow 2^\top \), and the answer is “definitely not”: because \(\Sigma ^{2^\top }\) is the space of co-spans in \(\Sigma \) under Phoa’s principle, this would imply that all upper bounds in \(\Sigma \) are least upper bounds, which is certainly not the case!

On the bright side, after disillusioning myself of the above, I did have a potentially promising idea for generalising some important notions from Alex Simpson’s Computational adequacy for recursive types in models of intuitionistic set theory that might give a clearer picture of the type-level iteration that is used to compute solutions to recursive domain equations in synthetic domain theory. We will see!