Post #1905744
2026-04-23 21:11 UTC
@maxsnew All propositions are "open" in a locale, because we can't even talk about non-open things. We can think about sublocales (which are not given by propositions but some kind of modality), but those are cursed. Maybe you can talk about openness in ionads though.
Replies (1)
-
@trebor@types.pl 2026-04-23 21:21
@maxsnew More precisely, morphisms 1 -> Ω in a sheaf topos over a locale correspond bijectively to opens in the locale. So it's difficult to talk about which propositions are open. The effective topos is IMO very unsatisfactory in terms of its connection to topology. For example the Baire space (Nat -> Nat) and the Cantor space (Nat -> Bool) are homeomorphic in Eff. (As a corollary, the "seemingly impossible functional program" is invalid in Eff.) A better substitute would be the realizability topos over something like the relative pca of Kleene's second algebra over its computable part, but I haven't completely worked through this.