这是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之间。