zstone1
zstone1
We've discussed at a handful of meetings that `topology.v` is too big at 8000 lines long. It causes at least 3 problems. 1. It makes it a pain to develop...
Creating an issue to track the various tasks on the proof of FTC. Apparently it's pretty hard, and requires work from many sources, and we're working on several streams: Track...
##### Motivation for this change as mentioned in the zulip, I've been having issues with pointedness being required on topology, and the interaction with weak subspaces/weak topologies. > I have...
I'm trying to build a project that recursively depends on a happy generated parser, and the eta-gradle plugin cannot build it. To get a repro: ``` 1. git clone https://github.com/typelead/eta-init...
A somewhat dramatic change in how things are organized. This breaks topology into a folder with a bunch of files in it. This has two big benefits - Dependencies are...
A grab-bag of results I'll need to split into separate reviews (once topology.v's split is done). This PR is mostly for bookkeeping, and stating my (new) roadmap for homotopies. My...
We already have proofs about curry/uncurry which require locally compact and uniform. One one hand, these results are critical for homotopy theory. One the other hand they are badly phrased...
Two related things. Now that pointed is gone from `topology`, we can canonically add topology/uniform/pseudometric on `set_val`. This now just a few easy instances. Then we define a mixin for...
Adding discrete topologies, uniformities, and metrics to the hierarchy. Cleans up a bunch of pre-HB issues, and now we can use `bool` directly instead of through a bunch of aliases....
A different manifestation of what might be the same bug as #446 but I can't tell from the outside ``` Variant testTy := A | B. HB.mixin Record Stack1 T...