ayberkt / formal-topology-in-uf

Formal Topology in Univalent Foundations (WIP).

Formal Topology in Univalent Foundations

Link to thesis.

This is the Agda development accompanying my (upcoming) master's thesis at Chalmers University of Technology to be titled Formal Topology in Univalent Foundations.

Note: This library is not actively maintained. The dependency cubical needs to be checked out to commit 09cc7134082573cf82436f5d317405812856f7f6. For an actively developed version of the locale theory development here, see the Locales in TypeTopology.

The approach to formal topology implemented here follows an idea of Thierry Coquand [0] to define formal topologies as posets endowed with interaction systems. The main novelty in this development is the definition of covering as an HIT. This seems to be necessary in the context of univalent type theory to avoid using a form of the axiom of choice.

The version of the code presented in the thesis will be archived whereas this repository (which is, as of now, mostly the same) will be maintained and developed further.

Question: what is formal topology?

Here is an answer by Giovanni Sambin [1]:

What is formal topology? A good approximation to the correct answer is: formal topology is topology as developed in (Martin-Löf's) type theory.

Also, this blog post by Mike Shulman contains interesting remarks about predicative mathematics and formal topology.

Overview

The main development comprises nine modules. If you are interested in reading the code, I suggest the following order:

1. Basis. Basic definitions of univalent type theory, many of which are imported from agda/cubical and some of which are adapted from Martín Escardó's introduction to HoTT/UF.
2. Poset.
3. Frame. A rudimentary development of frames.
4. Nucleus. The notion of a nucleus on a frame.
5. FormalTopology. Definition of a formal topology as an interaction system.
6. Cover. The cover relation induced by the structure of a formal topology.
7. CoverFormsNucleus. Contains the proof that the cover relation of a formal topology is a nucleus on the frame of downwards-closed subsets of its underlying poset.
8. UniversalProperty. Contains the proof that formal topologies present frames as expected.
9. CantorSpace. The definition of the formal Cantor topology along with a proof that it is compact.
10. Sierpinski. The formal topology of the Sierpinski space.

Clickable HTML

A rendering of the code in glorious clickable HTML can be accessed here.

Credits

This work was carried out under the supervision of Thierry Coquand.

References

0. Coquand, T. 1996. Formal Topology with Posets. http://www.cse.chalmers.se/~coquand/formal.html
1. Sambin, G. 2000. Formal Topology and Domains. Electronic Notes in Theoretical Computer Science. 35, (Jan. 2000), 177–190. DOI:https://doi.org/10.1016/S1571-0661(05)80742-X.

formal-topology-in-uf's Issues

Replace the propositional truncation defined in `Basis` with the one from `cubical`

Remove all dependencies to the standard library

The Level module is imported in various places, creating a dependency to the standard library. This can and should be circumvented by using the level stuff provided by cubical.

Prove Exercise II.1.5 from Stone Spaces

Show that a locale A is spatial iff each element of A can be expressed as a meet of prime elements. Show also that if A and B are spatial locales and f* : B -> A is left adjoint to f_* : A -> B then f^* preserves finite meets (i.e. is a frame homomorphism) iff f_* preserves prime elements.

Prove that the Sierpiński frame construction is correct

Prove Exercise I.2.2 from Stone Spaces

Stone Spaces, pg. 12:

Verify that a subset of a Boolean algebra A is an ideal (prime ideal) of A considered as a lattice
iff it is an ideal (prime ideal) of A considered as a ring.

Set up continuous deployment of Agda HTML to GitHub Pages