文件名称：UF中的形式拓扑：单价基础中的形式拓扑（WIP）
文件大小：85KB
文件格式：ZIP
更新时间：2024-03-09 19:43:53
topology homotopy-type-theory univalent-foundations univalent-mathematics formal-topologies
单价基础中的形式拓扑 。 这是我在Chalmers技术大学（即将发表的）硕士论文的标题为“单价基金会的形式拓扑”的Agda开发。 这里实现的形式拓扑方法遵循Thierry Coquand [0]的想法，将形式拓扑定义为具有坐姿。 这种发展的主要新颖之处在于将覆盖定义为HIT。 在单价类型理论的上下文中，这似乎有必要避免使用选择公理的形式。 本文中提供的代码版本将被存档，而该存储库（到目前为止，它几乎是相同的）将得到维护和进一步开发。 问题：什么是形式拓扑？ 这是乔瓦尼·萨宾[1]给出的答案： 什么是形式拓扑？ 正确答案的一个很好的近似是：形式拓扑是（Martin-Löf）类型理论中发展的拓扑。 另外，Mike Shulman的还包含有关谓词数学和形式拓扑的有趣评论。 概述 主要发展包括九个模块。 如果您有兴趣阅读代码，建议按照以下顺序进行： Basis 。 单价类型理论的基本
【文件预览】：
formal-topology-in-UF-master
----.github()
--------workflows()
----FormalTopology()
--------Main.lagda.md(440B)
--------CantorSpace.lagda.md(12KB)
--------SnocList.lagda.md(8KB)
--------Sierpinski.lagda.md(19KB)
--------Frame.lagda.md(40KB)
--------FormalTopology.lagda.md(3KB)
--------ProductTopology.lagda.md(2KB)
--------Ideal.lagda.md(2KB)
--------Basis.lagda.md(9KB)
--------UniversalProperty.lagda.md(15KB)
--------Regular.lagda.md(5KB)
--------Nucleus.lagda.md(12KB)
--------Makefile(66B)
--------Index.lagda.md(8KB)
--------Cofinality.lagda.md(2KB)
--------KuratowskiFinite.lagda.md(19KB)
--------generate_html.sh(472B)
--------FrameOfNuclei.lagda.md(31KB)
--------CoverFormsNucleus.lagda.md(5KB)
--------BaireSpace.lagda.md(2KB)
--------Prenucleus.lagda.md(1KB)
--------GaloisConnection.lagda.md(3KB)
--------Compactness.lagda.md(2KB)
--------Poset.lagda.md(20KB)
--------Cover.lagda.md(4KB)
----LICENSE(34KB)
----README.md(3KB)
----resources()
--------Agda.css(5KB)
----.gitignore(28B)