3 papers
cs.LO2026
Constructive and Predicative Locale Theory in Univalent Foundations
Ayberk Tosun
We develop locale theory constructively and predicatively in univalent foundations (UF), with a particular focus on the theory of spectral and Stone locales. In the context of UF,…
cs.LO2025
Internal Effectful Forcing in System T
Martin H. Escardo, Bruno da Rocha Paiva, Vincent Rahli +1
The effectful forcing technique allows one to show that the denotation of a closed System T term of type in the set-theoretical model is a continuous function $…
cs.LO2024
The Patch Topology in Univalent Foundations
Igor Arrieta, MartÃn Hötzel Escardó, Ayberk Tosun
Stone locales together with continuous maps form a coreflective subcategory of spectral locales and perfect maps. A proof in the internal language of an elementary topos was previo…