Pie 中构造函数的不相交

Question

是否可以证明 Pie 中构造函数的不相交性？

例如，是否有(Pi ((n Nat)) (-> (= Nat (add1 n) 0)) Absurd))类型的术语？

Answer 1

mietek 在 Freenode 的 ##dependent 上回答：

(claim disjoint-Nat (Pi ((n Nat)) (-> (= Nat (add1 n) 0) Absurd)))
(define disjoint-Nat
  (lambda (n prf)
    (replace
      prf
      (lambda (n) (iter-Nat n Absurd (lambda (_) Trivial)))
      sole)))

Pie 中构造函数的不相交

Disjointness of constructors in Pie

dependent-type