[Agda] Re: Agda Digest, Vol 87, Issue 24

[Martin Escardo]

On 21/11/12 11:04, Valeria de Paiva wrote:
> hey Martin,
>
> this is too cryptic for me:
>
> /The so-called "Curry-Howard isomorphism" seems to say that exists-forall
> are the same as Sigma-Pi. They are not the same. In fact, homotopy type
> theory, if you are following this recent trend, is re-introducing the
> distinction in a constructive context, and even at a syntactic,
> model-independent, level.
> /
> Can you elaborate, please?

I was aware that this assertion is risky.

I am happy to speak of e.g. the BHK-interpretation. You just say "let 
'exists' mean Sigma, and let 'forall' mean Pi.". And if you like, you 
make everything formal like Martin-Lof did very nicely.

But "Curry-Howard isomorphism" gives the impression that there are 
"exists" and "forall" out there, and they happen to correspond to 
"Sigma" and "Pi". (In a topos they don't, even though "exists" and 
"forall" obey the formal rules of intuitionistic logic.)

In HoTT, and even before HoTT, people define a "proposition" not to be a 
type, but instead a type with at most one element (suitably formulated). 
One also considers the "propositional reflection" of any type (similar 
to so-called bracket types), which hides (some part of the) 
computational content. Denote the propositional reflection of a type X 
by X* or [X]. Intuitively, X* is empty if X is empty, and X* has just 
one element if X* is inhabited (the trick is how to say this without 
using excluded middle).

Now you can define "exists x:X. A x" to mean (Sigma x:X. A x)*, and 
similarly "forall x:X. A x" to mean (Pi x:X. A x)*. These "exists" and 
"forall" obey the intuitionistic rules and behave very much like the 
"exists" and "forall" of a topos. Cf. Thorsten's message.

I hope this is not even more cryptic.

Best,
Martin