Post #1905745

@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.