例如，在 HoTT 书中引理 6.4.1 的证明中，在函数上归纳定义的函数简单地应用于路径
loop和refl，然后使用和之间的路径loop（refl可能是通过同余通过f）来构造和之间的f loop路径f refl：假设
loop = refl base. [...] 与x : Aandp : x = x，有一个由andf : S1 → A定义的函数，我们有f(base) :≡ xf(loop) := pp = 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)？
我在那里没有收到回复，所以我要在这里尝试，用具体的 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) ∎
它失败了，我想是因为我试图使用的“区间扩展性”：
无法将元变量实例化为
_342解决方案f (loop i) ≡ f base，因为它包含不在元变量i范围内或在元变量中不相关但在解决方案中相关的变量检查表达式
proofAt i是否具有类型时_A_342
尝试将其 eta 转换为 justproofAt_也失败了，但出于不同的原因（我认为通常没有路径的 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音译是什么？