[FOM] 'Salvaging' Voevodsky's talk

[Steven Awodey]

as someone involved in the development of the homotopical interpretation
of constructive type theory and the univalent foundations program, I would
like to point out that this program is independent of Vladimir's
provocative speculations regarding the consistency of PA -- as interesting
as those may be.

The research program of homotopy type theory and univalent foundations is
now being pursued by a group of people, including Vladimir.  More
information about this work can be found at:

www.homotopytypetheory.com

and the further links there.

Steve Awodey


On Sun, June 5, 2011 12:11 pm, Panu Raatikainen wrote:
> If I am not totally confused, there are versions of constructive type
> theory which prove the consistency of PA (right?). I wonder what Voevodsky
> would say about that?
>
> Best, Panu
>
>
>
> On Sat, Jun 04, 2011 at 06:51:22PM -0400, Timothy Y. Chow wrote:
>
>
>> The last part of his lecture argues that constructive type theory is a
>> better approach to foundations than traditional approaches are, because
>> it is more robust to possible contradictions.
>
>
> --
> Panu Raatikainen
>
>
> Ph.D., University Lecturer
> Docent in Theoretical Philosophy
>
>
> Theoretical Philosophy
> Department of Philosophy, History, Culture and Art Studies
> P.O. Box 24  (Unioninkatu 38 A)
> FIN-00014 University of Helsinki
> Finland
>
>
> E-mail: panu.raatikainen at helsinki.fi
>
>
> http://www.mv.helsinki.fi/home/praatika/
>
>
>
>