[FOM] Motivation for univalent foundations
Roger Bishop Jones
rbj at rbjones.com
Fri Jun 10 08:35:00 EDT 2011
On Monday 06 Jun 2011 19:32, Steven Awodey wrote:
> 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.
Given that Voevodsky's critique of ZFC as tainted by being
at least as inconsistent as PA (which we would normally
describe as being stronger than PA, and consider a merit)
fails to motivate many FOM researchers, it would be helpful
if an alternative reason for preferring Univalent
foundations over ZFC were on offer (or at least, for
interest if not preference).
This need not come in the form of a critique of ZFC, it
would be more informative if it were as accounts of positive
merits of Univalent foundations.
The homotopical interpretation of constructive type theory
is of interest, but it is not clear to me why this would
motivate the adoption of constructive type theories as
I have also yet to grasp in what way "univalent foundations"
differ from constructive type theory.
Perhaps Steve Awodey, who appears to have an interest in
univalent foundations which is independent of conjectures
about the consistency of PA could offer us an account of why
we should take an interest in this programme of research.
(I have looked at his survey, but did not come away with a
grasp of the foundational motivations).
More information about the FOM