问题标签 [homotopy-type-theory]

I'm writing an implementation for Curry-Howard isomorphism in scala, a family of proofs can be defined as an object implementing the following trait:

(the full code repo is uploaded to https://github.com/tribbloid/shapesafe/blob/djl/prove-debug/macro/src/main/scala/org/shapesafe/core/shape/unary/WithNames.scala)

In one particular case, the compiler got into a dead loop when 2 implicits are defined in a scope:

The compiler seems to be stuck on a cyclic proof resolution: it tries to fulfil lemma2 of theorem with itself. If I merge 2 implicits into 1, the problem disappeared:

So my questions are:

1. Why this could happen and what change of the scala compiler algorithm could eliminate any cyclic search for proves?

2. How to manually circumvent this error?

I also realised that the canonical implementation of homotopy type theory (https://github.com/siddhartha-gadgil/ProvingGround) actually does most of the inference in runtime, instead of compile-time, which seems to be defeating the purpose. Perhaps this bug is part of the reason?

我已经开始玩 Cubical Agda。我尝试做的最后一件事是构建整数类型（假设已经定义了自然数的类型），其方式类似于经典数学中的完成方式（参见wikipedia 上的整数构造）。这是

之后，我想定义加法

我现在卡在两个牙套之间的部分。x + a + (z + d) ≡ z + b + (x + c)询问类型术语。不想手动证明这一点，我想使用Cubical Agda 制造的环求解器。但我永远无法让它工作，甚至尝试将它设置为简单的环等式，如x + x + x ≡ 3 * x.

我怎样才能使它工作？有没有一个最小的例子使它适用于自然？库中有一个文件 NatExamples.agda，但它使您必须以复杂的方式重写您的等式。