区间外延性？

Question

I asked the following question on the CS SE:

For example, in the proof of lemma 6.4.1 in the HoTT book, a function inductively defined over a function is simply applied on paths loop and refl, and then a path between loop and refl is used (presumably by congruence via f) to construct a path between f loop and f refl:
Suppose that loop = refl base. [...] with x : A and p : x = x, there is a function f : S1 → A defined by f(base) :≡ x and f(loop) := p, we have
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
但这是否需要某种 "interval extensionality" 中间步骤？中间步骤的理由到底是什么立方型理论？我可以看到如何证明 ∀ i → f (loop i) = f (refl base i)，但是 "lift" 如何证明 <i> f (loop i) = <i> f (refl base i)？

我在那里没有收到回复，所以我打算在这里尝试，使用具体的 Agda 代码来支持它。

我正在尝试将上述证明转换为 Cubical Agda，如下所示。首先，给定 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)  ∎

它失败了，我认为是因为 "interval extensionality" 我正在尝试使用：

Cannot instantiate the metavariable _342 to solution f (loop i) ≡ f base since it contains the variable i which is not in scope of the metavariable or irrelevant in the metavariable but relevant in the solution

when checking that the expression proofAt i has type _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) !=< _344 ≡ _y_345 of type ;Agda.Primitive.Setω

那么，上述HoTT证明的正确CTT音译是什么？

Answer 1

请参阅 Saizan 的回答以获取与原始思路一致的解决方案。或者，有一个简单的解决方案：

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

或proof = cong (cong f) hyp。关键是hyp是二维的，而f作用于0维元素，所以f应该作用于hyp的0维分量。

Answer 2

路径确实有 eta 规则

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

然而，类型路径与区间 "I" 中的函数类型不同，因此有时您需要一个 lambda 抽象来在两种类型之间进行转换。（Lambda 和应用程序在两种类型之间临时重载）。

f loop 确实没有类型检查，甚至在 HoTT 中也没有。然而，本书将它用作 ap f loop 的 shorthand，其中 ap = cong 来自立方体库。

另外，你的证明可以完成，但你需要正确使用proofAt_：proof中的i维度是连接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)  ∎

区间外延性？

Interval extensionality?

agda

cubical-type-theory

homotopy-type-theory