1 citations · 2 across the 4 of their papers we have counts for
4 papers
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,…
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 $(\m…
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…
Patch Locale of a Spectral Locale in Univalent Type Theory
Ayberk Tosun, Martín Hötzel Escardó
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…