[FOM] alternative foundations?

Urs Schreiber urs.schreiber at googlemail.com
Sun Mar 23 09:56:32 EDT 2014

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


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


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.

More information about the FOM mailing list