Whitehead product

[aljungstrom]

This PR contains:

• A construction of the Whitehead product in terms of W : A * B → A ∨ B and a charaterisation of cofibres of W. (Prop 3.3.2. in Brunerie 2016).
• Some other minor lemmas relating to this proof
• A proof about homogeneity Π∙ which I for some reason thought might be useful in the future.

[kangrongji]

Very nice stuff! We are much closer towards Brunerie’s full paper, which I am really interested in.

Have you ever formalized anything about James construction? I wrote some codes on that, but only containing a few basic properties.

[aljungstrom]

Very nice stuff! We are much closer towards Brunerie’s full paper, which I am really interested in.

Have you ever formalized anything about James construction? I wrote some codes on that, but only containing a few basic properties.

I think that'd be the next step. My plan now is to first look into whether James could be avoided in the proof of lemma 3.4.4 for the case n = 2 (although only briefly, since this is probably too good to be true...)

I wrote some James stuff last year, but I remember I ran into some strange termination issues. So if you have something, I'd be really interested!:-)

[mortberg]

Very nice stuff! We are much closer towards Brunerie’s full paper, which I am really interested in.

Have you ever formalized anything about James construction? I wrote some codes on that, but only containing a few basic properties.

Where can we find your code on the James construction? I had a look and found a branch on your fork called "james", but I could not locate the new code

[kangrongji]

@mortberg I haven't upload the codes since it still has holes to fill in... I will keep on trying when I have some time.