文件名称：hott:伊德里斯的HoTT
文件大小：4KB
文件格式：ZIP
更新时间：2024-07-23 23:53:56
Idris
Idris 中同伦类型理论的一个小、不完整和不一致的形式化。 这表明，在 Idris 当前处理平等的情况下，任何在 Idris 中正式化 HoTT 的尝试都是不健全的。 问题是 Idris 具有异构相等性，以及异构相等性重写，这使我们能够证明True = False 。 在 HoTT 中，如果=是异质的，则True = False被居住是合理的。 所以真正的问题是内置的replace函数（和rewrite策略）将异构路径当作同构路径来处理。 hott.idr是主文件。 它包含路径、纤维、等价和单价的定义。 bad.idr包含矛盾。
【文件预览】：
hott-master
----.gitignore(6B)
----hott.idr(9KB)
----README.md(727B)
----bad.idr(727B)