Почему аксиома J принимает 2 х, давая подпись х, у? - PullRequest
Новая
       46

Почему аксиома J принимает 2 х, давая подпись х, у?

0 голосов
/ 16 октября 2018

Во-первых, я уже просмотрел несколько связанных материалов, в том числе книгу HoTT и этот вопрос .

Но я все еще в замешательстве и желаюобъяснение, свободное от Агды, но непосредственно от его математической формулы.После удаления точечной нотации J-аксиома затем говорит вот так, чья сигнатура типа полностью совпадает с ответом на вопрос, который я упомянул выше: 

J : forall {A : Set} {C : (x y : A) → (x ≡ y) → Set} →
                 (c : ∀ x → C x x refl) →
                 (x y : A) → (p : x ≡ y) → C x y p

, отмечая, что последняя строка просит наспредоставить х, у и р.Тогда почему 

J c x x refl = c x

, (единственное отличие в том, что я удалил обозначение точки)?Или сказать, почему второй x написан в x, а не в y?

Я действительно обдумал этот вопрос и получил объяснение, но не могу убедиться, что я прав.Типовая сигнатура J находится в пропозициональном мире, но ее определение в оценочном мире.Мы строим класс пропозиционального равенства шаг за шагом, но все оценочные равные переменные могут быть мгновенно переписаны друг в друга, и когда мы используем J, у нас уже должен быть x, по существу равный y (поскольку мы собираемся предоставить путь для этого),Но если мои рассуждения имеют безупречный смысл, оглядываясь назад на этот вопрос, почему мы снова пишем 

cong : ∀ { a b} { A : Set a }  { B : Set b }
   (f : A → B ) {m  n}  → m ≡ n → f m ≡ f n
cong f {x} {y} p = J {C = \x y p → f x ≡ f y}
                     (\_ → refl)
                     x y p

, где последняя строка дает x, y, p, но не x, x, p?

Ответы [ 2 ]

0 голосов
/ 24 октября 2018

J - аксиома индукции.Поскольку это аксиома, никаких доказательств не требуется.Аксиома гласит, что если вы можете предоставить свидетеля типа C x x refl, то C x y p можно построить для любых x и y, учитывая, что p является доказательством x ≡ y.

Доказательство в Агде на самом деле не является «полным» доказательством - нет видимого шага, который создает доказательства для C x y p для любых x, y и p.Видимая часть только устанавливает тот факт, что C x x refl может быть построен.Невидимая часть - это аксиома индукции, встроенная в систему проверки типа Agda, которая заключает, что это все, что нужно.

0 голосов
/ 17 октября 2018

Когда вы сопоставляете шаблон с p в refl в определении J, его тип уточняется с x ≡ y до x ≡ x (так как тип конструктора refl равен ∀ {x} -> x ≡ x,то есть он устанавливает оба индекса на x), что означает, что мы можем уточнить как левую, так и правую части на x ~ y, и именно поэтому y в шаблоне становится x (или, альтернативно, .x в Agda, чтобы сделать явным то, что это недоступный шаблон ), а также почему c x : C x x refl передается в правой части для типа результата C x y p.

...