文件名称：hott-limits:同伦类型理论中（同伦）极限的形式化
文件大小：47KB
文件格式：ZIP
更新时间：2024-07-21 16:16:23
Coq
热点限制 同伦类型理论中（同伦）限制的形式化，在 Coq HoTT 库上，如类型理论中的同伦限制一文中所述。 作者：Jeremy Avigad、Krzysztof Kapulkin、Peter LeFanu Lumsdaine。 概述 入门 组织 版本和兼容性 许可 概述 该库开发了图上类型图的（同伦）限制，在 Coq 中通过。 特别是，我们介绍了回拉及其基本理论（包括具体构造、通用性质、例子和两个回拉引理），一些关于图上一般图的类似基本理论（包括从乘积和均衡器构造一般限制），和一个应用程序，与纤维蛋白相关的长精确序列。 为了平衡学术出版物和软件库的竞争需求，该存储库包括库的稳定版本和不断发展的版本：大致上，伴随论文的稳定分支v1和不断发展的分支master 。 准确地说，一旦论文发表， v1分支上的标签MSCS将被永久冻结； v1的头部将至少更新，以保持与 HoTT 库的兼容性。
【文件预览】：
hott-limits-master
----Auxiliary.v(9KB)
----CommutativeSquares.v(4KB)
----Limits2.v(8KB)
----Pullbacks3_alt.v(29KB)
----PointedTypes.v(17KB)
----Pullbacks3.v(8KB)
----Pullbacks.v(33KB)
----Limits1.v(22KB)
----README.md(4KB)
----Makefile(1KB)
----Equalizers.v(727B)
----Arith.v(9KB)
----Fundamentals.v(9KB)
----Pullbacks2.v(8KB)
----.gitignore(39B)
----LongExactSequences.v(12KB)