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 に答える