[FOM] alternative foundations?

[Urs Schreiber]

On 3/23/14, Joseph Shipman <joeshipman at aol.com> wrote in parts:

> What's a well-known theorem for which HTT foundations makes the result much
> easier to find or prove than ZFC does?


For instance the Blakers-Massey theorem

  (e.g. http://ncatlab.org/nlab/show/Blakers-Massey+theorem ).

This appears as theorem 8.10.2 in the HoTT book

 http://ncatlab.org/nlab/show/HoTT+Book

and the formal proof in HoTT-Agda, by Lumdaine, Finster and Licata
(2013) is available here:

  https://github.com/dlicata335/hott-agda/blob/master/homotopy/BlakersMassey.agda

I'd suspect that already just fully formalizing the statement would be
unfeasible in other foundations. Certainly so if one regards the HoTT
proof as what it is, namely a generalization of the original theorem
from standard homotopy theory to more general homotopy toposes.

The same kind of comments would apply to all the results discussed in
chapter 8 of the HoTT book.