区间可拓性?

I asked the following question on the CS SE

例如,在霍特书中引理6.4.1的证明中,一个函数 函数上的归纳定义仅适用于路径 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

我们可以证明 环 那个 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) !=&书信电报; _344 ≡ _y_345 ;Agda.Primitive.Setω

那么,上述HoTT证明的正确CTT音译是什么?