# Interval extensionality?

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)?

Originally I was going to give an assurance that something like your extensionality principle must hold, but I decided to puzzle out enough cubical Agda to actually demonstrate the proof.

However, I should say that your all : ∀ i → f (loop i) = f (refl base i) is actually a digression. This is equivalent to a square with arbitrary sides, which looks like this:

$$\require{AMScd} \begin{CD} x @>all(0)>> x \\ @VpVV \Rightarrow @VVreflV \\ x @>>all(1)> x \end{CD}$$

but something with type p ≡ refl is actually more uniform than that, because if e has that type, then e i : x ≡ x regardless of i, which is more uniform than the above square (where e i : all i0 i ≡ all i1 i), and is equivalent to a square of the form:

$$\begin{CD} x @>refl>> x \\ @VpVV \Rightarrow @VVreflV \\ x @>>refl> x \end{CD}$$

But, if we have loop ≡ refl, we already have this sort of square, and applying f point-wise produces a new square of this type. So, the following code is accepted:

module Path
(S1 Z : Set)
(base : S1)
(loop : base ≡ base)
(f : S1 → Z)
(x : Z)

(sq : loop ≡ refl)
where
rfl : base ≡ base
rfl = refl

z : Z
z = f base

p : z ≡ z
p i = f (loop i)

zrfl : z ≡ z
zrfl = refl

hsq : p ≡ zrfl
hsq j i = f (sq j i)


So, the bit in the HoTT book is just a consequence of the composition of 'functions'.

The more arbitrary square can be expressed using the PathP type, which is also written _[_≡_] in cubical Agda, and the proof of equivalence to the ∀ type is:

module Square
(A : Set)
(x y : A)
(e₁ e₂ : x ≡ y)
(lines : ∀ i → e₁ i ≡ e₂ i)
where
f₀ : x ≡ x
f₀ = lines i0

f₁ : y ≡ y
f₁ = lines i1

square : (λ i → e₁ i ≡ e₂ i) [ f₀ ≡ f₁ ]
square i j = lines i j


If you want to fool around with cubical Agda yourself to try this out interactively, I've been using a recent Agda from the development branch with {-# OPTIONS --cubical #-}, along with this library.