7
$\begingroup$

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?

$\endgroup$
7
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ Would it be correct to say that because (p a) @ 0 is judgementally equal to (f a) we are allowed to rewrite it inside the lambda? So the difference is judgemental vs path equality. Makes sense to me. $\endgroup$ – WorldSEnder Sep 9 '18 at 0:04
  • 1
    $\begingroup$ I think that is correct to say. Expressions where a path is applied to 0 or 1 are judgmentally equal to the corresponding end point of the path, even though for arbitrary i you may not know the value. $\endgroup$ – Dan Doel Sep 9 '18 at 0:07

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.