Weakly contractible spaces initial PR

[felixpernegger]

Resolves #1633. T589 and T850 can still be generalised.
This PR makes me further belive that we should really require nonempty in P200.

The main reason for this, is so we can have a weak version of the very powerful whitehead theorem in pibase.

A somewhat similar (weaker) property is Aspehrical, but I dont think we gain much from adding that property as of now. (I am not aware of any interesting theorems)

Depends on #1758 and that the fact that the singleton is a CW complex (this should be done via Discrete => CW complex)

[prabau]

Do you mind first getting the CW complex PR finished before starting another one depending on it?

[prabau]

The previous work should include multiple PRs asserting that various spaces are are are not CW complex, etc.
Instead of rushing to add more properties and theorems.

The way we have been introducing new notions in pi-base is to first add the definition and some basic theorems. Then more involved theorems if any. Then examples and counterexample spaces.
And not rush from new property to new property.

@StevenClontz Do you want to comment? Am I off base?

[felixpernegger]

Do you mind first getting the CW complex PR finished before starting another one depending on it?

This is why I put it in draft :)
just wanted to write it down

[GeoffreySangston]

Please close this. This is just going to get out of date and is going to reserve property slots for a long time. Just save the files somewhere and open an Issue thread...

[felixpernegger]

How is it reserving property slots? it takes like 1 minute to update those

[StevenClontz]

I don't believe there's a problem with @felixpernegger making a draft PR that depends on another PR, as long as it's understood that there's no guarantee the first PR will be merged (and if so, this PR will need to be abandoned or refactored).

I'm going to look at this and #1758 a bit now.

[GeoffreySangston]

@felixpernegger @prabau @StevenClontz The first comment was overly harsh, but I do I think we should get back to using the Issue system for properties / spaces / theorems which have the potential to be relatively complex for pi-base contributions or to expand the character of the website. I think the "CW complex" property ended up being somewhat determined by a starting point that was decided on by one contributor. Then when larger suggestions were made there was an asymmetry (or at least this was my perception) because it would mean going against a PR that had already been worked on. That work was prioritized over suggestions which only existed as comments, though I thought it was important and should have shaped the direction of the PR from the outset. I think using issues let's more people contribute lower stakes ideas. They also let us gather more information that potentially won't get used explicitly but which can give us better context for shaping the PR.

For the case at hand, weakly contractible has been suggested at least twice in the past, so I think multiple people would like to have an opportunity to shape the direction of this property.

[felixpernegger]

fair enough, though I cant really think of an alternative way of defining this property.

[GeoffreySangston]

At this point we're probably just going to finish out this PR, which seems less than ideal to me, but I want to emphasize that. Getting to PRs quickly has its merits, but I think Issue system -> PR is a good process.

Hatcher defines Weak homotopy equivalence on page 352. Shouldn't we define it here? And that entails defining or linking to homotopy groups, so should we do one of those?

[GeoffreySangston]

@felixpernegger @prabau @StevenClontz Also one of the things I like about participating here is that people genuinely argue and discuss things. So if Felix for instance presented an argument to the effect of "yea but that was taking too long so let's just get going and it's been suggested so many times but nobody has pulled the trigger to make a PR", then maybe that should be considered (not that this is the argument, but that's sort of what I gather).