[FOM] Blakers-Massey in ZF and HoTT

[Hendrik Boom]

On Thu, Oct 23, 2014 at 09:35:54PM +0100, Paul B Levy wrote:

> 
> Suppose we teach a mathematics degree entirely inside HoTT.

I suppose a whole mathematics degree woukd usually start with a course 
in, say, calculus and analytic geometry?  It's perfectly possible to 
formulate it in type theory, and it will be just as type-theoretical 
just as much as it now is set-theoretical.  It doesn't even need the 
HoTT extensions to type theory.  Nor does it need to be tediously 
formal, the way it's done in Coq.  You can talk about types in English.

Then there might be a course that teaches how to build the complete 
number system, all the way upp to the complex numbers, from the natural 
numbers.  Also nicely type-theoretical.

It will be a while before they get to homotopy theory.  There's lots of 
elementary math they'd probably study first.  Linear Algebra.  
Differential equations.

Indeed if they are going to get a course in mathematical logic, it 
might even be based on type theory.  They might even get to start with 
a first-order type theory.

Eventually, probably after a course in Topology, and not concurrently,

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

By that time they will quite used to the type theoretical way of 
talking about things.  It won't faze tham.

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

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.  Students tend to learn generalities using 
specific examples.

I suspect very strongly that they will be able to prove it's "no".

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

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

--  hendrik