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
refl, and then a path between
refl is used (presumably by congruence via
f) to construct a path between
f loop and
loop = refl base. [...] with
x : Aand
p : x = x, there is a function
f : S1 → Adefined by
f(base) :≡ xand
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)?