Constructive and Predicative Locale Theory in Univalent Foundations
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, predicativity refers specifically to the development of mathematics without the use of propositional resizing axioms. The traditional approach to the predicative development of point-free topology is to work with presentations of locales known as formal topologies. Here, we take a different approach: we work directly with frames, keeping careful track of the universes involved and adopting certain size assumptions…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2603.01308
curl -X POST /api/v1/records/arxiv/2603.01308/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2603.01308/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'