这是 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

你的 "three-ended equality" 等同于一对相等性证明，在某种意义上，我们可以编写 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 所基于的形式系统）中，在相同项之间携带一对等式不会有太大收获，因为你唯一能做的就是这样的等式是对您操作的术语的类型执行强制转换。因此，项之间是否只有一个或两个等式证明通常并不重要。

由于添加了 univalence 公理，HoTT 的情况发生了一点变化，它允许我们在 types 之间使用等式证明] 以一种计算上有趣的方式。这是因为 HoTT 中 A = B 的证明可以是类型 A = B 之间的 any 双射。在那种情况下，teq A B C 的证明等同于两个双射：一个在 A 和 B 之间，另一个在 A 和 C 之间。

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

Is this a generalised path induction in COQ?

coq