First step of Stone duality for spectral locales

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.

GNU General Public License v3.0

228 stars 42 forks source link

First step of Stone duality for spectral locales #266

Closed ayberkt closed 5 months ago

ayberkt commented 5 months ago

Cleaned up version of PR #262.

ayberkt commented 5 months ago

@martinescardo I have now truncated the definition as discussed. This PR should be ready to merge.

I will add the definition that specifies the equivalence in #270 instead of this one. The reason is that the two branches were supposed to be independent, but they ended up getting a bit tangled. The definition that we discussed needs some things from the other branch. So I will keep this PR self-contained and minimal, and continue the progress we discussed today in #270, after we merge this.