区间可拓性

Question

I asked the following question on the CS SE

例如，在HoTT书中引理6.4.1的证明中，对函数进行归纳定义的函数简单地应用于路径loop和refl，然后使用loop和refl之间的路径(可能是通过f的同余)在f loop和f refl之间构造一条路径： 假设loop = refl base...。对于x : A和p : x = x，有一个由f(base) :≡ x和f(loop) := p定义的函数f : S1 → A，我们有 P=f(循环)= f(refl )= refl，但在立体的情况下，事情就不那么清晰了。f(loop)不是很好的类型，只有f(loop i)才是，对于某些i : I来说。但是上面的证明变成 P=f(循环i) =f(参考基i) = refl 但是，在中间的一步中，这难道不需要某种“区间扩展”吗？立体式理论中中间步骤的合理性究竟是什么？我可以看到如何证明∀ i → f (loop i) = f (refl base i)，但是如何将它“提升”到<i> f (loop i) = <i> f (refl base i)呢？

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

我正试图将上述证据转化为立体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类型时

试图将其转换为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音译是什么？

Answer 1

路径有eta规则

Demo/DemoPath.agda#L59

但是，类型路径与间隔"I“中的函数类型不一样，因此有时您需要一个lambda抽象来在这两种类型之间进行转换。(Lambda和应用程序在这两种类型之间是临时重载的)。

f loop确实不会打字，甚至在HoTT中也不会。然而，这本书用它作为ap f loop的简写，在那里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)  ∎

Answer 2

请参阅Saizan的答案，以获得原样的解决方案。或者，有一个简单的解决方案：

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

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