编程语言基础：Agda 描述

module plfa.part1.Equality where

我们在论证的过程中经常会使用相等性。给定两个都为 A 类型的项 M 和 N，我们用 M ≡ N 来表示 M 和 N 可以相互替换。在此之前，我们将相等性作为一个基础运算，而现在我们来说明如何将其定义为一个归纳的数据类型。

导入

本章节没有导入的内容。本书的每一章节，以及 Agda 标准库的每个模块都导入了相等性。我们在此定义相等性，导入其他内容将会产生冲突。

相等性

我们如下定义相等性：

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

用其他的话来说，对于任意类型 A 和任意 A 类型的 x，构造子 refl 提供了 x ≡ x 的证明。所以，每个值等同于它本身，我们并没有其他办法来证明值的相等性。这个定义里有不对称的地方，_≡_ 的第一个参数（Argument）由 x : A 给出，而第二个参数（Argument）则是由 A → Set 的索引给出。这和我们尽可能多的使用参数（Parameter）的理念相符。_≡_ 的第一个参数（Argument）可以作为一个参数（Parameter），因为它不会变，而第二个参数（Argument）则必须是一个索引，这样它才可以等于第一个。

我们如下定义相等性的优先级：

infix 4 _≡_

我们将 _≡_ 的优先级设置为 4，与 _≤_ 相同，所以其它算术运算符的结合都比它紧密。由于它既不是左结合，也不是右结合的，因此 x ≡ y ≡ z 是不合法的。

相等性是一个等价关系（Equivalence Relation）

一个等价关系是自反、对称和传递的。其中自反性可以通过构造子 refl 直接从相等性的定义中得来。我们可以直接地证明其对称性：

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

这个证明是怎么运作的呢？sym 参数的类型是 x ≡ y，但是等式的左手边被 refl 模式实例化了，这要求 x 和 y 相等。因此，等式的右手边需要一个类型为 x ≡ x 的项，用 refl 即可。

交互式地证明 sym 很有教育意义。首先，我们在左手边使用一个变量来表示参数，在右手边使用一个洞：

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym e = {! !}

如果我们进入这个洞，使用 C-c C-,，Agda 会告诉我们：

Goal: .y ≡ .x
————————————————————————————————————————————————————————————
e  : .x ≡ .y
.y : .A
.x : .A
.A : Set

在这个洞里，我们使用 C-c C-c e，Agda 会将 e 逐一展开为所有可能的构造子。此处只有一个构造子：

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = {! !}

如果我们再次进入这个洞，重新使用 C-c C-,，然后 Agda 现在会告诉我们：

 Goal: .x ≡ .x
 ————————————————————————————————————————————————————————————
 .x : .A
 .A : Set

这是一个重要的步骤—— Agda 发现了 x 和 y 必须相等，才能与模式 refl 相匹配。

最后，我们回到洞里，使用 C-c C-r，Agda 将会把洞变成一个可以满足给定类型的构造子实例。

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

我们至此完成了与之前给出证明相同的证明。

传递性亦是很直接：

trans : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans refl refl  =  refl

同样，交互式地证明这个特性是一个很好的练习，尤其是观察 Agda 的已知内容根据参数的实例而变化的过程。

合同性和替换性

相等性满足合同性（Congruence）。如果两个项相等，那么对它们使用相同的函数，其结果仍然相等：

cong : ∀ {A B : Set} (f : A → B) {x y : A}
  → x ≡ y
    ---------
  → f x ≡ f y
cong f refl  =  refl

两个参数的函数也满足合同性：

cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
  → u ≡ x
  → v ≡ y
    -------------
  → f u v ≡ f x y
cong₂ f refl refl  =  refl

在函数上的等价性也满足合同性。如果两个函数是相等的，那么它们作用在同一项上的结果是相等的：

cong-app : ∀ {A B : Set} {f g : A → B}
  → f ≡ g
    ---------------------
  → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl

相等性也满足替换性（Substitution）。如果两个值相等，其中一个满足某谓词，那么另一个也满足此谓词。

subst : ∀ {A : Set} {x y : A} (P : A → Set)
  → x ≡ y
    ---------
  → P x → P y
subst P refl px = px

谓词是对于某类型为 A 的值之上的命题；因为我们将命题视作类型，谓词则是对于 A 参数化的一个类型。例如，参考我们之前在 Relations 章节中的例子， even 和 odd 是自然数 ℕ 之上的谓词。（我们将在 Decidable 章节中比较谓词的两种表示方式：以归纳数据类型 A → Set 或者以布尔值函数 A → Bool。）

等式链

我们在此演示如何使用等式链来论证，正如本书中使用证明形式。我们将声明放在一个叫做 ≡-Reasoning 的模块里，与 Agda 标准库中的格式相对应。

module ≡-Reasoning {A : Set} where

  infix  1 begin_
  infixr 2 _≡⟨⟩_ step-≡
  infix  3 _∎

  begin_ : ∀ {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y  =  x≡y

  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
  step-≡ x y≡z x≡y  =  trans x≡y y≡z

  syntax step-≡ x y≡z x≡y  =  x ≡⟨  x≡y ⟩ y≡z

  _∎ : ∀ (x : A)
      -----
    → x ≡ x
  x ∎  =  refl

open ≡-Reasoning

这是我们第一次使用嵌套的模块。它包括了关键字 module 和后续的模块名、隐式或显式参数，关键字 where，和模块中的内容（在缩进内）。模块里可以包括任何形式的声明，也可以包括其他模块。嵌套的模块和本书每章节所定义的顶层模块相似，只是顶层模块不需要缩进。打开（open）一个模块会把模块内的所有定义导入进当前的环境中。

这也是我们第一次使用语法声明，它指明了左侧的项可以写成右边的语法形式。语法 x ≡⟨ x≡y ⟩ y≡z 继承了声明 step-≡ 时使用的中缀式声明 infixr 2，这种特殊的语法只要导入了 step-≡ 标识符就能使用。

除了引入带特殊语法的 step-≡ 外，我们也可以直接声明 _≡⟨_⟩′_：

_≡⟨_⟩′_ : ∀ {A : Set} (x : A) {y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
x ≡⟨ x≡y ⟩′ y≡z  =  trans x≡y y≡z

间接使用它的原因是 step-≡ 反转了实参的顺序，这样能让 Agda 更高效地执行类型推导。在 Lambda 一章中我们会遇到一些长等式链，因此效率是很重要的。

我们来看看如何用等式链证明传递性：

trans′ : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans′ {A} {x} {y} {z} x≡y y≡z =
  begin
    x
  ≡⟨ x≡y ⟩
    y
  ≡⟨ y≡z ⟩
    z
  ∎

根据其定义，等式右边会被解析成如下：

begin (x ≡⟨ x≡y ⟩ (y ≡⟨ y≡z ⟩ (z ∎)))

这里 begin 的使用纯粹是装饰性的，因为它直接返回了其参数。其参数包括了 _≡⟨_⟩_ 作用于 x、x≡y 和 y ≡⟨ y≡z ⟩ (z ∎)。第一个参数是一个项 x，而第二、第三个参数分别是等式 x ≡ y、y ≡ z 的证明，它们在 _≡⟨_⟩_ 的定义中用 trans 连接起来，形成 x ≡ z 的证明。y ≡ z 的证明包括了 _≡⟨_⟩_ 作用于 y、 y≡z 和 z ∎。第一个参数是一个项 y，而第二、第三个参数分别是等式 y ≡ z、z ≡ z 的证明，它们在 _≡⟨_⟩_ 的定义中用 trans 连接起来，形成 y ≡ z 的证明。最后，z ≡ z 的证明包括了 _∎ 作用于 z 之上，使用了 refl。经过化简，上述定义等同于：

trans x≡y (trans y≡z refl)

我们可以把任意等式链转化成一系列的 trans 的使用。这样的证明更加精简，但是更难以阅读。 ∎ 的小窍门意味着等式链化简成为的一系列 trans 会以 trans e refl 结尾，尽管只需要 e 就足够了，这里的 e 是等式的证明。

Exercise `trans` and `≡-Reasoning` (practice)

Sadly, we cannot use the definition of trans’ using ≡-Reasoning as the definition for trans. Can you see why? (Hint: look at the definition of _≡⟨_⟩_)

-- Your code goes here

等式链的另外一个例子

我们重新证明加法的交换律来作为等式链的第二个例子。我们首先重复自然数和加法的定义。我们不能导入它们（正如本章节开头中所解释的那样），因为那样会产生一个冲突：

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n  =  n
(suc m) + n  =  suc (m + n)

为了节约空间，我们假设两条引理（而不是证明它们）：

postulate
  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

这是我们第一次使用假设（Postulate）。假设为一个标识符指定一个签名，但是不提供定义。我们在这里假设之前证明过的东西，来节约空间。假设在使用时必须加以注意。如果假设的内容为假，那么我们可以证明出任何东西。

我们接下来重复交换律的证明：

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identity m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

论证的过程和之前的相似。我们在不需要解释的地方使用 _≡⟨⟩_，我们可以认为 _≡⟨⟩_ 和 _≡⟨ refl ⟩_ 是等价的。

Agda 总是认为一个项与其化简的项是等价的。我们之所以可以写出

  suc (n + m)
≡⟨⟩
  suc n + m

是因为 Agda 认为它们是一样的。这也意味着我们可以交换两行的顺序，写出

  suc n + m
≡⟨⟩
  suc (n + m)

而 Agda 并不会反对。Agda 只会检查由 ≡⟨⟩ 隔开的项是否化简后相同。而书写的顺序合不合理则是由我们自行决定。

练习 `≤-Reasoning` (延伸)

章节 Relations 中的单调性证明亦可以用相似于 ≡-Reasoning 的，更易于理解的形式给出。相似地来定义 ≤-Reasoning，并用其重新给出加法对于不等式是单调的证明。重写 +-monoˡ-≤、+-monoʳ-≤ 和 +-mono-≤ 的定义。

-- 请将代码写在此处。

重写

考虑一个自然数的性质，比如说一个数是偶数。我们重复之前给出的定义：

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

在前面的部分中，我们证明了加法满足交换律。给定 even (m + n) 成立的证据，我们应当可以用它来做 even (n + m) 成立的证据。

Agda 对这种论证有特殊记法的支持——我们之前提到过的 rewrite 记法。来启用这种记法，我们只用编译程序指令来告诉 Agda 什么类型对应相等性：

{-# BUILTIN EQUALITY _≡_ #-}

我们然后就可以如下证明求证的性质：

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev  rewrite +-comm n m  =  ev

在这里，ev 包括了所有 even (m + n) 成立的证据，我们证明它亦可作为 even (n + m) 成立的证据。一般来说，关键字 rewrite 之后跟着一个等式的证明，这个等式被用于重写目标和任意作用域内变量的类型。

交互性地证明 even-comm 是很有帮助的。一开始，我们先给左边的参数赋予变量，给右手边放上一个洞：

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev = {! !}

如果我们进入洞里，输入 C-c C-,，Agda 会报告：

Goal: even (n + m)
————————————————————————————————————————————————————————————
ev : even (m + n)
n  : ℕ
m  : ℕ

现在我们加入重写：

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev rewrite +-comm n m = {! !}

如果我们再次进入洞里，并输入 C-c C-,，Agda 现在会报告：

Goal: even (m + n)
————————————————————————————————————————————————————————————
ev : even (m + n)
n  : ℕ
m  : ℕ

目标里的参数被交换了。现在 ev 显然满足目标条件，输入 C-c C-a 会用 ev 来填充这个洞。命令 C-c C-a 可以进行自动搜索，检查作用域内的变量是否和目标有相同的类型。

多重重写

我们可以多次使用重写，以竖线隔开。举个例子，这里是加法交换律的第二个证明，使用重写而不是等式链：

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ zero    n  rewrite +-identity n             =  refl
+-comm′ (suc m) n  rewrite +-suc n m | +-comm′ m n  =  refl

这个证明更加的简短。之前的证明用 cong suc (+-comm m n) 作为使用归纳假设的说明，而这里我们使用 +-comm m n 来重写就足够了，因为重写可以将合同性考虑在其中。尽管使用重写的证明更加的简短，使用等式链的证明能容易理解，我们将尽可能的使用后者。

深入重写

rewrite 记法实际上是 with 抽象的一种应用：

even-comm′ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm′ m n ev with   m + n  | +-comm m n
...                  | .(n + m) | refl       = ev

总的来着，我们可以在 with 后面跟上任何数量的表达式，用竖线分隔开，并且在每个等式中使用相同个数的模式。我们经常将表达式和模式如上对齐。这个第一列表明了 m + n 和 n + m 是相同的，第二列使用相应等式来证明的前述的断言。注意在这里使用的点模式（Dot Pattern），.(n + m)。点模式由一个点和一个表达式组成，在其他信息迫使这个值和点模式中的值相等时使用。在这里，m + n 和 n + m 由后续的 +-comm m n 与 refl 的匹配来识别。我们可能会认为第一种情况是多余的，因为第二种情况中才蕴涵了需要的信息。但实际上 Agda 在这件事上很挑剔——省略第一条或者更换顺序会让 Agda 报告一个错误。（试一试你就知道！）

在这种情况中，我们也可以使用之前定义的替换函数来避免使用重写：

even-comm″ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm″ m n  =  subst even (+-comm m n)

尽管如此，重写是 Agda 工具箱中很重要的一部分。我们会偶尔使用它，但是它有的时候是必要的。

莱布尼兹（Leibniz）相等性

我们使用的相等性断言的形式源于 Martin-Löf，于 1975 年发表。一个更早的形式源于莱布尼兹，于 1686 年发表。莱布尼兹断言的相等性表示不可分辨的实体（Identity of Indiscernibles）：两个对象相等当且仅当它们满足完全相同的性质。这条原理有时被称作莱布尼兹定律（Leibniz’ Law），与史波克定律紧密相关：「一个不造成区别的区别不是区别」。我们在这里定义莱布尼兹相等性，并证明两个项满足莱布尼兹相等性当且仅当其满足 Martin-Löf 相等性。

莱布尼兹相等性一般如下来定义：x ≐ y 当每个对于 x 成立的性质 P 对于 y 也成立时成立。可能这有些出乎意料，但是这个定义亦足够保证其相反的命题：每个对于 y 成立的性质 P 对于 x 也成立。

令 x 和 y 为类型 A 的对象。我们定义 x ≐ y 成立，当每个对于类型 A 成立的谓词 P，我们有 P x 蕴涵了 P y：

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

我们不能在左手边使用 x ≐ y，取而代之我们使用 _≐_ {A} x y 来提供隐式参数 A，这样 A 可以出现在右手边。

这是我们第一次使用等级（Levels）。我们不能将 Set 赋予类型 Set，因为这会导致自相矛盾，比如罗素悖论（Russell’s Paradox）或者 Girard 悖论。不同的是，我们有一个阶级的类型：其中 Set : Set₁，Set₁ : Set₂，以此类推。实际上，Set 本身就是 Set₀ 的缩写。定义 _≐_ 的等式在右手边提到了 Set，因此签名中必须使用 Set₁。我们稍后将进一步介绍等级。

莱布尼兹相等性是自反和传递的。自反性由恒等函数的变种得来，传递性由函数组合的变种得来：

refl-≐ : ∀ {A : Set} {x : A}
  → x ≐ x
refl-≐ P Px  =  Px

trans-≐ : ∀ {A : Set} {x y z : A}
  → x ≐ y
  → y ≐ z
    -----
  → x ≐ z
trans-≐ x≐y y≐z P Px  =  y≐z P (x≐y P Px)

对称性就没有那么显然了。我们需要证明如果对于所有谓词 P，P x 蕴涵 P y，那么反方向的蕴涵也成立。

sym-≐ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → y ≐ x
sym-≐ {A} {x} {y} x≐y P  =  Qy
  where
    Q : A → Set
    Q z = P z → P x
    Qx : Q x
    Qx = refl-≐ P
    Qy : Q y
    Qy = x≐y Q Qx

给定 x ≐ y 和一个特定的 P，我们需要构造一个 P y 蕴涵 P x 的证明。我们首先用一个谓词 Q 将相等性实例化，使得 Q z 在 P z 蕴涵 P x 时成立。 Q x 这个性质是显然的，由自反性可以得出，由此通过 x ≐ y 就能推出 Q y 成立。而 Q y 正是我们需要的证明，即 P y 蕴涵 P x。

我们现在来证明 Martin-Löf 相等性蕴涵了莱布尼兹相等性，以及其逆命题。在正方向上，如果我们已知 x ≡ y，我们需要对于任意的 P，将 P x 的证明转换为 P y 的证明。我们很容易就可以做到这一点，因为 x 与 y 相等意味着任何 P x 的证明即是 P y 的证明。

≡-implies-≐ : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → x ≐ y
≡-implies-≐ x≡y P  =  subst P x≡y

因为这个方向由替换性可以得来，如之前证明的那样。

在反方向上，我们已知对于任何 P，我们可以将 P x 的证明转换成 P y 的证明，我们需要证明 x ≡ y：

≐-implies-≡ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → x ≡ y
≐-implies-≡ {A} {x} {y} x≐y  =  Qy
  where
    Q : A → Set
    Q z = x ≡ z
    Qx : Q x
    Qx = refl
    Qy : Q y
    Qy = x≐y Q Qx

此证明与莱布尼兹相等性的对称性证明相似。我们取谓词 Q，使得 Q z 在 x ≡ z 成立时成立。那么 Q x 是显然的，由 Martin Löf 相等性的自反性得来。从而 Q y 由 x ≐ y 可得，而 Q y 即是我们所需要的 x ≡ y 的证明。

（本部分的内容由此处改编得来： ≐≃≡: Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically 作者：Andreas Abel、Jesper Cockx、Dominique Devries、Andreas Nuyts 与 Philip Wadler，草稿，2017）

全体多态

正如我们之前看到的那样，不是每个类型都属于 Set，但是每个类型都属于类型阶级的某处， Set₀、Set₁、Set₂等等。其中 Set 是 Set₀ 的缩写，此外 Set₀ : Set₁，Set₁ : Set₂，以此类推。当我们需要比较两个属于 Set 的类型的值时，我们之前给出的定义是足够的，但如果我们需要比较对于任何等级 ℓ，两个属于 Set ℓ 的类型的值该怎么办呢？

答案是全体多态（Universe Polymorphism），一个定义可以根据任何等级 ℓ 来做出。为了使用等级，我们首先导入下列内容：

open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

我们将构造子 zero 和 suc 重命名至 lzero 和 lsuc，为了防止自然数和等级之间的混淆。

等级与自然数是同构的，有相似的构造子：

lzero : Level
lsuc  : Level → Level

Set₀、Set₁、Set₂ 等名称，是下列的简写：

Set lzero
Set (lsuc lzero)
Set (lsuc (lsuc lzero))

以此类推。我们还有一个运算符：

_⊔_ : Level → Level → Level

给定两个等级，返回两者中较大的那个。

下面是相等性的定义，推广到任意等级：

data _≡′_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl′ : x ≡′ x

相似的，下面是对称性的推广定义：

sym′ : ∀ {ℓ : Level} {A : Set ℓ} {x y : A}
  → x ≡′ y
    ------
  → y ≡′ x
sym′ refl′ = refl′

为了简洁，我们在本书中给出的定义将避免使用全体多态，但是大多数标准库中的定义，包括相等性的定义，都推广到了任意等级，如上所示。

下面是莱布尼兹相等性的推广定义：

_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y

之前，签名中使用了 Set₁ 来作为一个值包括了 Set 的类型；而此处，我们使用 Set (lsuc ℓ) 来作为一个值包括了 Set ℓ 的类型。

标准库中的大部分函数都泛化到了任意层级。例如，以下是复合的定义。

_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
  → (B → C) → (A → B) → A → C
(g ∘ f) x  =  g (f x)

更多关于层级的信息可以从Agda 文档中查询。

标准库

标准库中可以找到与本章节中相似的定义。Agda 标准库将 _≡⟨_⟩_ 定义为 step-≡，它反转了参数的顺序。标准库还定义了一个语法宏，它可以在你导入 step-≡ 时被自动导入，它能够恢复原始的参数顺序：

-- import Relation.Binary.PropositionalEquality as Eq
-- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

这里的导入以注释的形式给出，以防止冲突，如引言中解释的那样。

Unicode

本章节使用下列 Unicode：

≡  U+2261  等同于 (\==, \equiv)
⟨  U+27E8  数学左尖括号 (\<)
⟩  U+27E9  数学右尖括号 (\>)
∎  U+220E  证毕 (\qed)
≐  U+2250  趋近于极限 (\.=)
ℓ  U+2113  手写小写 L (\ell)
⊔  U+2294  正方形向上开口 (\lub)
₀  U+2080  下标 0 (\_0)
₁  U+2081  下标 1 (\_1)
₂  U+2082  下标 2 (\_2)

导入

相等性