Эквивалентна ли дефиниционная и пропозициональная экстенсиональность поверх теории интенсиональных типов?

Question

Я читаю статью о теории экстенсиональных типов в n-lab и упоминает два способа сделать теорию экстенсионных типов экстенсиональной.

1. Определение: Добавить правило p:Id(x,y) => x===y
2. Предложение: добавьте одно из следующего к теории типов
   • аксиома UIP
   • аксиома К
   • аксиома с указанием Id((a,b_1),(a,b_2)) => Id(b_1,b_2), где (a,b_1) и (a,b_2) обе зависимые пары
   • добавить сопоставление шаблонов без ограничений, как в оригинальной Agda

У меня вопрос, эти два пути эквивалентны?

В частности, если да, можно ли вывести p:Id(x,y) => x===y из аксиомы K или UIP?

Answer 1

N-лаборатория понимает, что для теории типов быть экстенсиональной, довольно своеобразно. Это имеет смысл, если вас больше всего интересует, можно ли расширить тип Id однолистностью, а это не так, если у вас UIP.

(1) подразумевает (2) (используя числа из вопроса), поэтому это не соответствует однозначности.

(1) - это правило, которое более традиционные источники ассоциируют с названием «теория типов экстенсиональных».

Однако (2) не подразумевает (1), так как каноничность типа Id для теории, подобной Агде, показала бы, что любое доказательство Id в пустом контексте является рефлексивностью, в то время как (1) подразумевает расширение функций .