Blakers-Massey about book

[dlicata335]

fixed

[DanGrayson]

I took a look at the new phrasing of Blakers-Massey:

(1) Why not phrase Blakers-Massey in terms of two maps C -> X and C -> Y, instead of in terms of a fibration C -> XxY? It would sound more standard. If the proof involves fibrant replacement of the map C -> XxY, that needn't be revealed in the statement of the theorem.

(2) The hypothesis is too weak to support the conclusion, since it focuses on just two fibers. Thus the conclusion will be false if X or Y is not connected. But don't add connectedness of X and Y as a separate hypothesis, since it's cleaner to speak of the maps C->X and C->Y having a connectedness property.

(3) If C : XxY -> U, then in X \sqcup^C Y one must replace C by the total space (type) of the fibration, so as to match the definition of pushout. But it would be better to start out with C as a type, instead.

(4) In what sense is the pushout constructor \glue a map C(x,y) \rightarrow X \sqcup^C Y ? That says glue produces a point in the pushout, but it produces a path. Because of this I can't tell whether the conclusion of the theorem is what it's supposed to be.

Perhaps we should introduce a definition for what it means for a square to be n-connected (all iterated homotopy fibers are n-connected). Then say that if C->X is i-connected and C->Y is j-connected, the resulting pushout square is i+j-connected.

Reopening.

[peterlefanulumsdaine]

I took a stab at rewriting the statement of B-M in 6cf8787 (Dan L, I hope that’s OK?). How does it look to you (Dan G) now? I’ve addressed most of your comments, except for the suggestion of defining n-connectedness of a square — since it’s only used in this one case, I think it would obscure the content of the theorem a bit.

New version.

[DanGrayson]

It looks good now. I had to guess twice to figure out that (f,g) denotes the induced map C -> XxY, which should be said. In fact, I've made that change in 8fe4407. Feel free to close after looking.

[dlicata335]

OK, there was some mismatch in my version because I think pushouts should be defined for a dependent type C(x,y), not for two maps f : C -> X and g : C -> Y. But that's not what the chapter on pushouts does, so this phrasing is alright with me.

(1) was a symptom of this
(2) was a bug; you additionally need C(x0,y0)
(3) was a symptom of this
(4) was a typo; glue's type would be C(x,y) -> inl x = inr y

[guillaumebrunerie]

Pushouts can be defined for a dependent type but I don’t think we should do it this way. For instance pushouts are often used to glue a cell to some space and phrasing such a pushout with a dependent type would give something rather strange.

[DanGrayson]

They're also used to make mapping cones and mapping cylinders, for arbitrary maps f : X -> Y.