warning: repository reorganization

Stream: Infinity-Cosmos

[Emily Riehl]

I wanted to give a heads up that I just pushed a reorganization of the InfinityCosmos repository which closes down our local "Mathlib" folder entirely. I found it confusing to keep track of what only existed here and what was in mathlib already. Anything novel that was in there is now in the "ForMathlib" folder instead.

[Emily Riehl]

For the most part the "ForMathlib" folder contains files that aren't in mathlib at all. The exception is the "Basic" file under "SimplicialCategory" but I didn't feel confident I understood the state of that, so I decided not to touch it.

[Emily Riehl]

One particular note for @Jack McKoen: there's a new file on "SimplicialSet" called "MorphismProperty" which contains the definition of a trivial fibration. I just suggested that @Nima Rasekh define isofibrations for us there.