这是 COQ 中的广义路径归纳吗？

Question

我正在学习同伦类型理论 (HoTT) 及其与 COQ 的关系。 尤其是身份类型的路径归纳概念对我来说还是很神秘的。
因此，我用 COQ 做了一些实验。

让我们从一个使用路径归纳的标准相等类型的简单引理开始：

Lemma eq_sym: forall (x y:nat), x = y -> y = x.
intros.
apply (match H in (_ = y0) return y0 = x with eq_refl => eq_refl end).
Defined.

现在让我们看看这是否是对 COQ "eq" 类型的特殊处理。因此，让我们用一个类似的对称引理定义一个新的相等类型（仅适用于 nat）：

Inductive est  (x : nat) : nat -> Prop :=
    est_refl:  est x x.  

Lemma est_sym: forall (x y:nat), est x y -> est y x.
intros.
apply (match H in (est _ y0) return est y0 x with est_refl => est_refl x end).
Defined. 

好的，这与标准“=”类型的工作方式相同。
现在让我们概括一下：

Inductive tri  (x : nat) : nat->nat->Prop :=
    tri_refl:  tri x x x.

Lemma tri_sym: forall (x y z:nat), tri x y z -> tri z x y.
intros.
apply (match H in (tri _ y0 z0) return tri z0 x y0  with tri_refl => tri_refl x end).
Defined.

我的问题是：
这与HoTT理论有什么关系？
这是不是 HoTT 的一部分的广义路径归纳吗？

Answer 1

您的“三端相等”相当于一对相等证明，在某种意义上，我们可以编写 Coq 函数在两种形式之间来回转换。 （这些是下面摘录中的 eq_of_teq 和 teq_of_eq 术语。）

Section Teq.

Variable T : Type.

Inductive teq (x : T) : T -> T -> Prop :=
| teq_refl : teq x x x.

Definition teq_of_eq {x y z} (e1 : x = y) (e2 : x = z) : teq x y z :=
  match e1 in _ = y' return x = z -> teq x y' z with
  | eq_refl => fun e2 =>
    match e2 in _ = z' return teq x x z' with
    | eq_refl => teq_refl x
    end
  end e2.

Definition eq_of_teq1 {x y z} (te : teq x y z) : x = y :=
  match te in teq _ y' z' return x = y' with
  | teq_refl => eq_refl
  end.

Definition eq_of_teq2 {x y z} (te : teq x y z) : x = z :=
  match te in teq _ y' z' return x = z' with
  | teq_refl => eq_refl
  end.

Definition teq_eq_teq x y z (te : teq x y z) :
  teq_of_eq (eq_of_teq1 te) (eq_of_teq2 te) = te :=
  match te as te' in teq _ y' z' return teq_of_eq (eq_of_teq1 te') (eq_of_teq2 te') = te' with
  | teq_refl => eq_refl
  end.

Definition eq_teq_eq1 x y z (e1 : x = y) (e2 : x = z) :
  eq_of_teq1 (teq_of_eq e1 e2) = e1 :=
  match e1 as e1' in _ = y' return eq_of_teq1 (teq_of_eq e1' e2) = e1' with
  | eq_refl =>
    match e2 as e2' in _ = z' return eq_of_teq1 (teq_of_eq eq_refl e2') = eq_refl with
    | eq_refl => eq_refl
    end
  end.

Definition eq_teq_eq2 x y z (e1 : x = y) (e2 : x = z) :
  eq_of_teq2 (teq_of_eq e1 e2) = e2 :=
  match e1 as e1' in _ = y' return eq_of_teq2 (teq_of_eq e1' e2) = e2 with
  | eq_refl =>
    match e2 as e2' in _ = z' return eq_of_teq2 (teq_of_eq eq_refl e2') = e2' with
    | eq_refl => eq_refl
    end
  end.

End Teq.

teq_eq_teq、eq_teq_eq1 和 eq_teq_eq2 引理表明，来回转换不会改变我们开始使用的术语；因此，两种表示是等价的。从这个意义上说，Coq 并没有比 HoTT 更强大的表达能力，因为我们可以定义一个teq。

在基本的 Martin-Löf 类型理论（HoTT 所基于的形式系统）中，通过在相同项之间携带一对等式并不会获得太多收益，因为使用这样的等式你唯一能做的就是对您操作的术语类型执行强制转换。因此，术语之间是否只有一个或两个相等证明通常并不重要。

由于添加了单价公理，HoTT 中的情况发生了一些变化，这使我们能够以一种有趣的计算方式使用类型 之间的相等性证明。这是因为在HoTT 中A = B 的证明可以是A = B 类型之间的任意双射。在这种情况下，teq A B C 的证明相当于两个双射：一个在 A 和 B 之间，另一个在 A 和 C 之间。