Fixed typo in proof of function extensionality using the interval type, so it also works for functions of type A -> B instead of only A -> A. ;)
Ignore Keynote file.