[FOM] Motivation for univalent foundations

[Roger Bishop Jones]

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 
foundation systems.

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).

Roger Jones