Interval extensionality?

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.

But in a cubical setting, things are not so clear-cut. f(loop) is not well-typed, only f(loop i) is, for some i : I. But then that above proof becomes

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

but doesn't that need some kind of "interval extensionality" in the middle step? What exactly is the justification of the middle step in cubical type theory? I can see how to prove ∀ i → f (loop i) = f (refl base i), but how does one "lift" that to <i> f (loop i) = <i> f (refl base i)?

I haven't received a response there so I'm going to try here, with concrete Agda code to back it.

I am trying to turn the above proof into Cubical Agda as follows. First, given p, the definition of f is straightforward:

  hyp : loop ≡ refl {x = base}

  p : x ≡ x

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

We can prove pointwise along loop that f (loop i) ≡ f (refl i):

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

(to see why, here it is in more detail:

  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                 ∎

)

but if I try to prove it for the whole thing:

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

it fails, I would think because of the "interval extensionality" I am trying to use:

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

trying to eta-convert it to just proofAt_ also fails, but for a different reason (and I think there is, in general, no eta conversion for paths):

  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ω

So, what is the correct CTT transliteration of the above HoTT proof?

Answer 1

Paths do have eta rules

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

however the type path is not the same as the type of functions from the interval "I", so sometimes you need a lambda abstraction just to convert between the two types. (Lambda and application are ad-hoc overloaded between the two types).

f loop indeed does not typecheck, not in even in HoTT. However the book uses it as a shorthand for ap f loop, where ap = cong from the cubical library.

Also, your proof can be completed, but you need to use proofAt_ correctly: the i dimension in proof is the one connecting cong f loop and refl {x = f base}, so you want to provide i as the second argument of 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

See Saizan's answer for a solution along the original lines. Alternatively, there is a simple solution:

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

Or proof = cong (cong f) hyp. The key is that hyp is two-dimensional, and f acts on 0-dimensional elements, so f should be applied to the 0-dimensional components of hyp.