实凝聚同伦类型论中的布劳威尔不动点定理
范畴论
2017-04-26 v3 代数拓扑
逻辑
摘要
我们将同伦类型论与公理化凝聚结合，使用一种“伴随逻辑”的变体在内部表达后者，其中离散化与余离散化模态通过“清晰变量”的判定形式主义来刻画。这产生了我们称之为“空间”与“凝聚”的类型论，其中的类型可被视为具有独立的拓扑与同伦结构。这些类型论随后可用于形式化研究拓扑产生同伦论（“基本 -群胚”或“形状”）的过程，将同伦类型论的“等同”与拓扑的“连续路径”解耦。在一种称为“实凝聚”的进一步精炼中，形状由来自实数的连续映射决定，正如经典代数拓扑那样。这使我们能够形式化地复现同伦论对拓扑的一些经典应用。作为例子，我们证明了布劳威尔不动点定理。
引用
@article{arxiv.1509.07584,
title = {Brouwer's fixed-point theorem in real-cohesive homotopy type theory},
author = {Michael Shulman},
journal= {arXiv preprint arXiv:1509.07584},
year = {2017}
}
备注
75 pages; v2: small changes, characterized the codiscrete reals, renamed a couple axioms; v3: some reorganization and new results, including Brouwer's continuity theorem and a constructive approximate Brouwer's fixed-point theorem, to appear in MSCS