dependent-type - Pie中构造函数的不相交性

Question

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

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

标签： dependent-type

Answer 1

在 Freenodemietek上回答：##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)))