Idris 中同伦类型理论的一个小、不完整和不一致的形式化。 这表明，在 Idris 当前处理平等的情况下，任何在 Idris 中正式化 HoTT 的尝试都是不健全的。
问题是 Idris 具有异构相等性，以及异构相等性重写，这使我们能够证明True = False 。 在 HoTT 中，如果=是异质的，则True = False被居住是合理的。 所以真正的问题是内置的replace函数（和rewrite策略）将异构路径当作同构路径来处理。
hott.idr是主文件。 它包含路径、纤维、等价和单价的定义。 bad.idr包含矛盾。
