Interval extensionality?
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 @&gt;all(0)&gt;&gt; x \\
@VpVV \Rightarrow @VVreflV \\
x @&gt;&gt;all(1)&gt; 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 @&gt;refl&gt;&gt; x \\
@VpVV \Rightarrow @VVreflV \\
x @&gt;&gt;refl&gt; 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.