[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> > For example, if I write a proof in Agda, using function extensionality, > is it a program? No. But if I write --cubical in the header of my Agda > program and import a suitable cubical library, then yes. I can define an > integer using function extensionality so that Agda will get stuck trying > to compute it but Cubical Agda won't (and I have done it in the cubical > library as an illustrative example). No wrong answers here, but I'm curious: What makes a proof in Agda using functional extensionality different in your mind from a function that takes a proof of functional extensionality as an input, and then returns the proof? Is the latter a program? Is the latter a program once you turn on --cubical, since now it has inputs? Do programs need to have realizable inputs? To my knowledge, a proof is a very (very) specific kind of program. > What makes it more specific? In my mind, you can certainly view any program in any language as a proof in some logical system, even if the logical system is not actually implemented as the language's type checker, and even if the corresponding logic is unsound. A proof in an unsound logic is still a proof, I think---just a possibly useless one (possibly useful, though, since you can have incorrect assumptions and still sometimes prove things that in no way rely on them). On Tue, May 18, 2021 at 2:10 PM Martin Escardo <[email protected]> wrote: > > > On 18/05/2021 21:58, Martin Escardo wrote: > > (and it is > > probably independent). > > In univalent type theories. > > Martin > >
