LEAN 类型理论之注解（Annotations of LEAN Type Theory）-- 相等类型（Equality Type）

        《何谓相等 (Equality)，在类型理论(Type Theory)语境下》 与 《转化（conversion and reduction）后的相等（Equality）》，两文中，已对相等（Equality）的概念进行了描述，此文，是LEAN中，通过定义一个用于表达（express）相等（equality）的归纳类型（Inductive Type），即，相等类型（Equality Type）。

        相等类型（Equality Type）表达了，给定一个类型 α，类型α里的元素自身相等（equals itself），即其自反性（reflexivity）。记为

        α:Uₗ, a:α ⊢ eqₐ := μt: α→ℙ .(refl: t a)

        析：

        给定 类型α  及 类型为α 的变量 a，有相等类型 eqₐ，其定义为 μt: α→ℙ .(refl: t a)。 也就是说，eqₐ 是类型函数，α→ℙ，（输入为类型α 的值，输出为命题（proposition））；其构建函数为 refl: t a，因 t 的类型为 α→ℙ，有 t a =  eqₐ a，其类型为 ℙ （Proposition），即 refl: eqₐ a :ℙ ，为命题的证明（proof of proposition）。

        也就是说，给定一个类型 α 及该类型的变量 a，有相等类型 eqₐ，其含义为，给定另一个类型 α的值 a' ，生成出一个判断（Judgement / Proposition），a 与 a' 相等，即 eqₐ a' :ℙ ，与其构建函数 refl 的类型（eqₐ a :ℙ）相同，因此，构建函数 refl，用于构建该判断的证明（proof）。构建函数 refl的定义(refl: t a) 中的 a，引用的是 ⊢ 符号左边的变量 a，也是 eqₐ 中的 a，因此，构建函数 refl 表达了，当 a 与 a' 是同一个时，两者相等，即作为 eqₐ a' :ℙ 的证明（proof），

refl: eqₐ a :ℙ = refl: eqₐ a' :ℙ（a = a'） 

        关键点：(refl: t a) 和 eqₐ 中的变量 a，是同一个变量a，来自其假设（Assumptions），即 ⊢ 符号左边的变量 a。

        换个看法，将相等类型看作 eq，而非 eqₐ，有

        eq : α:Uₗ → a:α → b: α→ ℙ

        即，给定对应的输入，eq 返回一个命题（proposition）, 即 a 与 b 相等。

        其构建函数 refl （short for reflexivity） 是：

refl: a:α  → (eq α a a)

       即，其输入只有一个值，来自 ⊢ 符号左边的变量 a，说明了，该值等于其自身，即自反性（reflexivity）。

        也就是说，相等类型表达了，只有任何类型的元素，其自身相等（reflexivity）。

        同时，LEAN类型系统定义了，定义上相等（Definitioanl Equality）的表示达可以相互替换（substitute equals for equals），由此，当两个表达式，通过使用各种转化规则，最终规范化成相同元素，则两个表达式相等，即 eq a b，where a⇔ b。

        另外，因相等类型只有一个无参数的构建函数，refl: t a，所以，相等类型的使用函数是 Large Elimination，即其使用函数的目标类型（Target Type）可以指向任意类型宇宙（Universes）。

        使用 LEAN 语言的语法表达如下：

inductive Eq : α → α → Prop where| refl (a : α) : Eq a a

        注：LEAN语言 是 LEAN类型理论中的表达式语法（Syntax of Expression） 的 具象化（Embodiment），用于在代码层级上，表达 LEAN类型理论中定义的所有表达式（Expression）。