以下是一种可能的方法，即尝试对本段进行字面解释：
当证明一个陈述时 E:N→U 关于所有的自然数，只要证明一下就足够了 0 以及 succ(n) ，假设它持续 n ，即我们建造 ez:E(0) 以及 es:∏(n:N)E(n)→E(succ(n)) .
来自hott手册（第5.1节）。
以下是代码实现的计划：
为“某些财产”的陈述提供证据意味着什么 P 适用于所有自然数”。下面，我们将使用

trait Forall[N, P[n <: N]]:
   inline def apply[n <: N]: P[n]

签名人在哪里 apply -方法本质上说是“为了所有人” n <: N ，我们可以找到 P[n] ".
注意，方法声明为 inline . 这是确保 ∀n.P(n) 是构造性的，并且在运行时可执行（但是，请参见编辑历史记录以获取具有手动生成的见证条件的备选方案）。
假设自然数的某种归纳法则。下面，我们将使用以下公式：

If
    P(0) holds, and
    whenever P(i) holds, then also P(i + 1) holds,
 then
    For all `n`, P(n) holds

我认为应该有可能 derive 这样的归纳法则使用了一些元编程工具。
为归纳原理的基本情况和归纳情况撰写证明。 ??? 利润
代码如下所示：

sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat

type plus[a <: Nat, b <: Nat] <: Nat = a match
  case O => b
  case S[n] => S[n plus b]

trait Forall[N, P[n <: N]]:
  inline def apply[n <: N]: P[n]

trait NatInductionPrinciple[P[n <: Nat]] extends Forall[Nat, P]:
  def base: P[O]
  def step: [i <: Nat] => (P[i] => P[S[i]])
  inline def apply[n <: Nat]: P[n] =
    (inline compiletime.erasedValue[n] match
      case _: O => base
      case _: S[pred] => step(apply[pred])
    ).asInstanceOf[P[n]]

given liftCoUpperbounded[U, A <: U, B <: U, S[_ <: U]](using ev: A =:= B):
  (S[A] =:= S[B]) = ev.liftCo[[X] =>> Any].asInstanceOf[S[A] =:= S[B]]

type NatPlusZeroEqualsNat[n <: Nat] = (n plus O) =:= n

def trivialLemma[i <: Nat]: ((S[i] plus O) =:= S[i plus O]) =
  summon[(S[i] plus O) =:= S[i plus O]]

object Proof extends NatInductionPrinciple[NatPlusZeroEqualsNat]:
  val base = summon[(O plus O) =:= O]
  val step: ([i <: Nat] => NatPlusZeroEqualsNat[i] => NatPlusZeroEqualsNat[S[i]]) = 
    [i <: Nat] => (p: NatPlusZeroEqualsNat[i]) =>
      given previousStep: ((i plus O) =:= i) = p
      given liftPreviousStep: (S[i plus O] =:= S[i]) =
        liftCoUpperbounded[Nat, i plus O, i, S]
      given definitionalEquality: ((S[i] plus O) =:= S[i plus O]) =
        trivialLemma[i]
      definitionalEquality.andThen(liftPreviousStep)

def demoNat(): Unit = {
  println("Running demoNat...")
  type two = S[S[O]]
  val ev = Proof[two]
  val twoInstance: two = new S[S[O]]
  println(ev(twoInstance) == twoInstance)
}

它编译、运行和打印：

true

这意味着我们已经成功地对类型为的可执行证据项调用了递归定义的方法 two plus O =:= O .
一些进一步的评论
这个 trivialLemma 是必要的 summon 在另一个里面 given 不要意外地生成递归循环，这有点烦人。
分离 liftCo -方法 S[_ <: U] 是需要的，因为 =:=.liftCo 不允许类型构造函数具有上界类型参数。 compiletime.erasedValue + inline match 太棒了！它自动生成某种运行时小控件，允许我们对“擦除”类型进行模式匹配。在我发现这一点之前，我试图手动构造适当的见证条件，但这似乎根本没有必要，它是免费提供的（请参阅编辑历史记录以了解手动构造见证条件的方法）。