Flawed argument in the proof of function extensionality in cubical type theory?
The expression:

\(a : A) -&gt; (p a) @ 0


parses as:

\(a : A) -&gt; ((p a) @ 0)


So this is applying p a : Path B (f a) (g a) to the 0 point. This reduces to f a, because it is the beginning point of the path. It's essentially doing the same thing as the earlier step, which beta reduced the (&lt;i&gt; ...) @ 0 to (...)[i := 0], except p a looks abstract to us, but that doesn't matter, because we know what it reduces to when applied to 0 (or 1) based only on its type.

So, it's not using function extensionality to prove extensionality. What it's doing is taking advantage of the fact that Path types are similar to function types, and that the two Path types in funExt are 'just' functions with different argument order (so it flips them).