martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220 stars 40 forks source link

Step 2 of PR #217 #255

Closed ayberkt closed 4 months ago

ayberkt commented 4 months ago

Step 2 of PR #217 is now ready to review.

ayberkt commented 4 months ago

P.S. I will send the proof of spectrality of the Sierpiński locale (which was also in PR #217) in Step 3.

ayberkt commented 4 months ago

@tomdjong This got merged already, but let me know if you have any comments or suggestions.

ayberkt commented 4 months ago

Thanks @tomdjong! I’ll address these in a separate PR.