1

在依赖类型理论中有一个相等类型。通常在定义这种类型时，会引入一些实用程序，即 cong 和 subst。它们的表现力如何？是否有可能用消除器表达我们所能表达的一切以与他们平等？

4

1 回答 1

1

不，您不能仅使用 cong、subst 和 Eliminator 来证明身份证明的唯一性。

uip : {α : Level} {A : Set α} {x y : A} -> (p q : x ≡ y) -> p ≡ q

这是解释：http ://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/

于 2014-03-25T10:57:03.317 回答