В теории зависимо типизированных типов есть тип равенства. Обычно при определении этого типа вводится ряд утилит, а именно cong и subst. Насколько они выразительны? Можно ли выразить все, что можно, с помощью элиминатора на равенство с ними?
Тип Cong, subst и равенство в языках программирования с зависимой типизацией
Ответы (1)
Нет, вы не можете доказать уникальность удостоверений личности только с помощью cong, subst и destroyator.
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/
person
user3237465
schedule
25.03.2014
Я думаю, вопрос был в том, можем ли мы использовать subst и cong для доказательства стандартного правила исключения J. Я не уверен, каков ответ на этот вопрос, но я тоже предполагаю, что нет.
- person Jesper; 25.03.2014
Да, вопрос был в возможности выразить правило исключения с помощью этих примитивов. Насколько я понимаю, вы упомянули Axiom K, верно? (ncatlab.org/nlab/show/axiom+K)
- person Konstantin Solomatov; 26.03.2014
Ах, теперь я понял. Простите за это. Да, мой ответ касается аксиомы К.
- person user3237465; 26.03.2014
