[FOM] Blakers-Massey in ZF and HoTT

[Paul B Levy]

Dear Urs,

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 
induced topology.

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.

Best regards,
Paul