hottIdris中的HoTT形式化问题

在Idris中，同伦类型理论（HoTT）的一个小、不完整且不一致的形式化被展示出来。当前Idris在处理平等时存在问题，任何在Idris中正式化HoTT的尝试都会是不可行的。问题源于Idris具有异构相等性（heterogeneous equality）以及异构相等性重写（heterogeneous equality rewriting），这使得我们能够证明True = False。在HoTT中，如果‘=’是异质的，那么True = False是合理的居住。因此，真正的问题在于内置的replace函数（和rewrite策略）将异构路径误当作同构路径来处理。主文件hott.idr定义了路径（path）、纤维（fiber）、等价（equivalence）和单价（unit）的概念。而bad.idr则包含了矛盾的示例。