[Agda] Re: Agda Digest, Vol 87, Issue 24
Martin Escardo
m.escardo at cs.bham.ac.uk
Wed Nov 21 13:07:55 CET 2012
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
More information about the Agda
mailing list