- Minneapolis, MN
- https://mzhang.io
- Joined on
2020-07-21
Decide on a research project
Decided on: formalize spectral sequences (Floris van Doorn's PHD thesis)
- https://florisvandoorn.com/talks/Bonn2018spectralsequences.pdf
- formalized previously, but not in cubical -…
Chapter 6: Higher inductive types
Study Theorem 3.2.2
I have most of the proof written down, but the biggest thing that confuses me is:
Thus, applying (3.2.4) to
f(\mathbf{2})(u)
and (3.2.3), we obtain an element of\mathbf{0}
.
This means…