[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
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.
More information about the FOM
mailing list