refactor: Unstructured

[Jlh18]

I have dumped the current progress with the unstructured model stuff in this PR. I moved the NaturalModel stuff into a subdirectory. I commented out the Natural.Interpretation.lean file in HoTTLean.lean because it was conflicting with the new Unstructured.Interpretation.lean, so lake build is no longer keeping track of the NaturalModel files.

TODO:

2. Define UHomSeq.Pis and UHomSeq.Sigmas using polymorphic sigmas and pis.
3. Generalize the groupoid model constructions to have polymorphic sigmas and pis. (I'm a bit worried about the polymorphic Pis in the groupoid model actually, I remember having to restrict the universe levels somewhat.)
4. (after 2.) finish refactoring the interpretation