[FOM] alternative foundations?
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