Argumento defeituoso na prova da extensionalidade da função na teoria do tipo cúbico?

Estou lendo as palestras sobre a teoria dos tipos cúbicos neste repositório do github . Na aula 1, o autor define a extensionalidade da função da seguinte maneira:

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

e escreve

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

Eu não sigo. Especificamente, quando substituímos (p a) @ 0por f aminha mente, usamos o seguinte fato: \(a : A) -> (p a) @ 0 = f apara reescrever (vamos dar nomes para os lados esquerdo e direito) fpa = \(a : A) -> (p a) @ 0em fa = \(a : A) -> f a. Mas não é isso, por si só, usando extensionalidade de função f = fpa, g = fa?

Se não me engano, esse argumento é circular. Alguém pode esclarecer?

A expressão:

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

analisa como:

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

Então, isso se aplica p a : Path B (f a) (g a)ao 0ponto. Isso se reduz a f a, porque é o ponto inicial do caminho. Ele está basicamente fazendo o mesmo que na etapa anterior, que reduziu o beta (<i> ...) @ 0para (...)[i := 0], exceto p aparece abstrato para nós, mas isso não importa, porque sabemos ao que ele se reduz quando aplicado a 0(ou 1) com base apenas em seu tipo.

Portanto, não está usando a extensionalidade da função para provar a extensionalidade. O que está fazendo é tirar proveito do fato de que os Pathtipos são semelhantes aos tipos de função e que os dois Pathtipos funExtsão funções 'just' com ordem de argumento diferente (para que sejam invertidos).