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

Question

I am reading the lectures about cubical type theory in this github repo. In lecture 1 the author defines function extensionality the following way:

funExt (A B : U) (f g : A -> B)
       (p : (x : A) -> Path B (f x) (g x)) :
       Path (A -> B) f g = <i> \(a : A) -> (p a) @ i

and writes

To see that this makes sense compute the end-points of the path:

  (<i> \(a : A) -> (p a) @ i) @ 0 = \(a : A) -> (p a) @ 0
                                  = \(a : A) -> f a
                                  = f

I don't follow. Specifically, when we replace (p a) @ 0 with f a in my mind we use the following fact: \(a : A) -> (p a) @ 0 = f a to rewrite (let's give names to the left and right side) fpa = \(a : A) -> (p a) @ 0 into fa = \(a : A) -> f a. But isn't this by itself using function extensionality with f = fpa, g = fa?

If I am not mistaken, this argument is circular. Can anyone clarify?

Answer 1

The expression:

\(a : A) -> (p a) @ 0

parses as:

\(a : A) -> ((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 (<i> ...) @ 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).