Интервал экстенсиональности?

Question

Я задал следующий вопрос в CS SE :

Например, при доказательстве леммы 6.4.1 в книге HoTT функция, индуктивно определенная надФункция просто применяется к путям loop и refl, а затем используется путь между loop и refl (предположительно, с помощью конгруэнции через f) для построения пути между f loop и f refl:

Предположим, что loop = refl base.[...] с x : A и p : x = x, есть функция f : S1 → A, определяемая f(base) :≡ x и f(loop) := p, у нас есть

p = f(loop) = f(refl base) = refl x.

Но в кубической установкене все так ясно.f(loop) не правильно напечатано, только f(loop i) для некоторых i : I.Но тогда это вышеупомянутое доказательство становится

p = <i> f (loop i) = <i> f (refl base i) = refl x

, но разве для этого не нужна какая-то "расширенность интервала" на среднем этапе?Что именно является обоснованием среднего шага в теории кубического типа?Я могу видеть, как доказать ∀ i → f (loop i) = f (refl base i), но как можно «поднять» это до <i> f (loop i) = <i> f (refl base i)?

Я не получил ответа там, поэтому я собираюсь попробовать здесь, сконкретный код Агды, чтобы поддержать его.

Я пытаюсь превратить приведенное выше доказательство в Кубическую Агду следующим образом.Во-первых, учитывая p, определение f является простым:

  hyp : loop ≡ refl {x = base}

  p : x ≡ x

  f : S¹ → A
  f base = x
  f (loop i) = p i

Мы можем доказать точечно вдоль loop, что f (loop i) ≡ f (refl i):

  proofAt_ : ∀ i → f (loop i) ≡ f base
  proofAt i = cong (λ p → f (p i)) hyp

(чтобы понять почему, здесь это более подробно:

  proofAt_ : ∀ i → f (loop i) ≡ f base
  proofAt i = begin
    f (loop i)             ≡⟨ cong (λ p → f (p i)) hyp ⟩
    f (refl {x = base} i)  ≡⟨⟩
    f base                 ∎

)

, но если я попытаюсь доказать это в целом:

  proof : p ≡ refl
  proof = begin
    (λ i → p i)             ≡⟨⟩
    (λ i → f (loop i))      ≡⟨ (λ i → proofAt i) ⟩
    (λ i → f base)          ≡⟨⟩
    (λ i → refl {x = x} i)  ∎

это не удается, я думаю, из-за "расширения интервалов", которое я пытаюсь использовать:

Невозможно создать метаварию _342 для решения f (loop i) ≡ f base, поскольку она содержит переменную iкоторый не входит в сферу действия метавариабельной переменной или не имеет отношения к метавариабельной, но имеет отношение к решению

при проверке того, что выражение proofAt i имеет тип _A_342

, пытаясь установитьпреобразовать его в proofAt_ также не удается, но по другой причине (и я думаю, что в общем случае нет преобразования eta для путей):

  proof : p ≡ refl
  proof = begin
    (λ i → p i) ≡⟨⟩
    (λ i → f (loop i)) ≡⟨ proofAt_ ⟩
    (λ i → f base) ≡⟨⟩
    (λ i → refl {x = x} i) ∎

((i : I) → f (loop i) ≡ f base)! = <<code>_344 ≡ _y_345 типа ;Agda.Primitive.Setω

Итак, какова правильная транслитерация CTT вышеупомянутого доказательства HoTT?

Answer 1

Пути имеют правила eta

https://github.com/Saizan/cubical-demo/blob/master/examples/Cubical/Examples/AIM_Demo/DemoPath.agda#L59

однако путь к типу не совпадает с типом функций из интервала «I», поэтому иногда требуется лямбда-абстракцияпросто конвертировать между двумя типами.(Лямбда и приложение перегружены специальным образом между двумя типами).

f loop действительно не проверяет тип, даже в HoTT.Однако книга использует его как сокращение для ap f loop, где ap = cong из кубической библиотеки.

Кроме того, ваше доказательство может быть завершено, но вам нужно правильно использовать proofAt_: iизмерение в proof является соединением cong f loop и refl {x = f base}, поэтому вы хотите указать i в качестве второго аргумента proofAt_.

proof : p ≡ refl
proof = begin
  (λ i → p i)             ≡⟨⟩
  (λ i → f (loop i))      ≡⟨ (λ i j → proofAt j i) ⟩
  (λ i → f base)          ≡⟨⟩
  (λ i → refl {x = x} i)  ∎

Answer 2

См. Ответ Сайзана для решения в соответствии с оригинальными линиями.Альтернативно, есть простое решение:

proof : p ≡ refl
proof i j = f (hyp i j)

или proof = cong (cong f) hyp.Ключ в том, что hyp является двумерным, а f действует на 0-мерные элементы, поэтому f следует применять к 0-мерным компонентам hyp.