[FOM] Blakers-Massey in ZF and HoTT
Paul B Levy
P.B.Levy at cs.bham.ac.uk
Thu Oct 23 16:35:54 EDT 2014
According to my limited understanding, working inside ZF, you can (i)
define HoTT as an object language, (ii) define its model using
simplicial sets, (iii) take Lumsdaine, Finster and Licata's HoTT proof.
This gives you a ZF proof of Blakers-Massey. Am I correct?
And a very nice proof it is, because the formalization of HoTT and its
model is once and for all, so the next time you want to prove a theorem
of this kind, you need only give an appropriate HoTT proof.
Therefore we should perhaps encourage anyone proving Blakers-Massey in
ZF, whether formally or informally, to choose this way. (Although there
may be other insights or benefits to be had from other proofs; I really
don't know, as it's outside my area of expertise.)
However, I would like to question the premise of your challenge, viz.
that Lumsdaine, Finster and Licata's formalization (LFL) constitutes *by
itself* a proof of Blakers-Massey, without any need to formalize the
simplicial set model.
Suppose we teach a mathematics degree entirely inside HoTT. The
students attend a course entitled "Homotopy", which is about properties
of types. The "circle" and "sphere" are defined to be particular
(higher inductive) types, and the students learn to calculate their
higher homotopy groups. They also learn LFL.
Concurrently, they attend a course entitled "Topology" in which
"topological space" and "continuous map" are defined. The "topological
circle" and "topological sphere" are defined to be, respectively,
subsets of R^2 and R^3 consisting of points of unit magnitude, with the
At the end of both courses, the teacher asks the students: "Are the
topological circle and the topological sphere homeomorphic?"
What will the students answer? Can they leverage what they have learnt
in the Homotopy course to help them prove the answer is "No"? What was
the good of attending a homotopy course if it doesn't enable them to
answer such a simple question?
It seems to me (and I could well be wrong) that there is only one way
for the students to answer this question. That is to ignore everything
they learnt in the Homotopy course, and directly define the higher
homotopy groups of a topological space and painstakingly calculate them
for the topological circle and sphere. Just like students taking a
traditional ZF-based degree.
So now the students have learnt two subjects, "homotopy" and
"topological homotopy". They are completely separate - from the
viewpoint of the students, who live inside HoTT and don't know its
models. Only the latter enables them to answer the homeomorphism
question. And if the students want to know whether topological
Blakers-Massey holds, LFL will not (I think) be of use to them.
More information about the FOM