這是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之間。