[FOM] Blakers-Massey in ZF and HoTT

[Paul B Levy]

Dear Hendrik, thanks for your reply but I don't think you're addressing 
my point.

>  > 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?
>
> I suppose one *could* teach homotopy without ever mentioning that it's
> relevant to topological spaces and continuous mapping, but it seems a
> stupid way to do it.

I fully agree with you, but unfortunately, inside HoTT, the subject of 
homotopy of higher inductive types is separate from topology.  So the 
teacher is unable to make that important connection.

> Students tend to learn generalities using specific examples.
>
> I suspect very strongly that they will be able to prove it's "no".

How?  I suggested one way:

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

What are you suggesting as an alternative?

> You don't need set theory to express the models.  You can formulate
> these models in type theory -- it's not even all that different from the
> set-theoretical version.

So your suggestion is that the students define HoTT as an object 
language along with its model(s), then copy the proofs they learnt in 
the Homotopy course into the object language?  Indeed that would work, 
regardless of whether the metalanguage is ZF or HoTT, but it hardly 
affects my point that the students cannot *deduce* the answer they need 
from the theorems they learnt in the Homotopy course.

Paul

-- 
Paul Blain Levy
School of Computer Science, University of Birmingham
http://www.cs.bham.ac.uk/~pbl