本文假设读者已经装了 NuPRL5 的 VM/要到了帳號并照著 http://nuprl.org/html/02cucs-NuprlManual-02overview.pdf 做基操。
这是向略懂 dependent type 的人的 NuPRL 教程，介紹这一最神/传奇的定理证明器。你不需要会 Haskell，但是至少要能理解 untyped lambda calculus，最好会点 OCaml/SML，最理想是 LCF ML，因为这是 NuPRL 的 Tactic 语言，而且它沒正式的 language report。Lisp 麻，会用 Emacs 程度就可以了，在 NuPRL 里几本用不上。
这文章只能向有 Agda/Coq/HOL/PVS/Metamath 经验的介绍下 NuPRL 了，因为完全 normie 的话像我一样出见 NuPRL 怕是不太可能有过了。
Equality in CTT
我们先来看 equivalence。不好意思让你们失望了，NuPRL 里沒有 ADT。所以 NuPRL 的 $a = b \in T$ 是个 primitive，如果 a 和 b 不等就是个空集，相等则有唯一成员 $*$ ，相当于 unit type。
值得一提的是，在 Agda 用的 ITT 中，一个 value 只能和自己相等，但在 CTT，因为有 quotient type 的概念，你还可以定义一个类型使两个不同的 value 相等。
given equality relation $E$ on type $T$
$a = b \in T/\!/E \iff a E b$
Number, Subset type(refinement type/subtype by comprehension)
连 Equality 都 primitive 了，NuPRL 的 Integer 也是 primitive 的。所以就不要想 Peano number 了。
自然数的定义直接上 refinement type。
$\mathbb{N} == \{i:\mathbb{Z}\ |\ 0\leq i\}$
Unit, then to Binary
equality 已經成了 primitive，別的就不用都重新定义了。
$a \in T == a = a\in T$
Unit 也就这么定义了
$Unit == 0 \in \mathbb{Z}$
Boolean:
$\mathbb{B} == Unit + Unit$
是不是发现了什么？
沒错，NuPRL 沒有用来 pattern match 的 data constructor。毕竟是用 tactic 做证明的啉，case split 有 tactic，要 pattern match 又沒用。
结语(划掉)
不好意思，我们还没做证明。那現在就可以来一个了
$*>\!> 0 = 0 \in \mathbb{Z}\ {by}\ \texttt{Auto}$
好，证完了。反正用 Auto Tactic 就对了。
Subtyping
你们好多人说 Subtyping 难，然而在 NuPRL 里 subtyping 如吃飯喝水一样自然。首先看看这句定义
A is a subtype of B, written A ≤ B, if a value of type A can be supplied wherever a value of type B is demanded.
然后把这给忘了吧，因为 CTT 的 subtyping 是这么定义的
A is a subtype of B ( $A \sqsubseteq B$ ) iff $a = a' \in A \implies a=a' \in B$
这是一个外延性定义。
自然地
$\{x:A\ |\ P(x) \} \sqsubseteq A$
Void, Top, Intersection over a family
$ u=v \in \bigcap\limits_{x:A}{B(x)} \iff \forall x \in A. u=v \in B(x)$
注意不要和 intersection type 搞混了，虽然它们是有关系。
Void 就是 Empty type。它是个 primitive。当然，并不代表你不能用 $\{x:\mathbb{Z}\ |\ x 在一个有 subtyping 的 type theory 里，Top 可不能和 Unit 混在一起了 (说的就是你，Agda！) Intersection over a family 中 A 为 empty 时，B(x) 的 B 就是 a functions from Empty to some type 了，因为从 empty 可以 derive anything，所以这样就是 Top, where $A \sqsubseteq Top$ 了。当然 Agda 用 $\top$ 表示 Unit 不是沒有道理的，因为 $A^0 \cong 1$ (即从 empty 到所有类型的 function 只有一个)嚒。 $A(given\ B)=\bigcap\limits_{x:A}{B(x)}$ if x is free in B. 这叫做 Guarded Type，作用放之后讲。不过現在我们可以用 $Void(given\ Void)$ 来定义 Top。