[FOM] Blakers-Massey in ZF and HoTT

[Paul Levy]

Since sending this message, my attention has been drawn to the  
following very interesting thread, which discusses some similar issues.

https://groups.google.com/forum/#!topic/HomotopyTypeTheory/AI5yAWzCVLQ

I would like to say the following.  I greatly prefer the kind of  
discussion on that thread, which hops back and forth between HoTT  
theorems on the one hand and models and metatheorems on the other, to  
the HoTT book, which is conducted entirely inside HoTT and therefore  
doesn't mention models.  At the risk of being extremely provocative, I  
feel that the former is science and the latter is more like  
propaganda.  I do not think one can give a well-motivated introduction  
to HoTT without mentioning models.  By contrast, I think it is  
perfectly fine to introduce ZF in the traditional way without  
mentioning models.

Paul






On 23 Oct 2014, at 21:35, Paul B Levy wrote:

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

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