Michael Zhang michael
michael pushed to master at school/type-theory 2024-05-23 16:29:32 +00:00
cbf61d6a96 Update .gitattributes
michael commented on issue school/type-theory#12 2024-05-23 15:19:29 +00:00
Decide on a research project

Decided on: formalize spectral sequences (Floris van Doorn's PHD thesis)

michael closed issue school/type-theory#12 2024-05-23 15:19:29 +00:00
Decide on a research project
michael pushed to master at school/type-theory 2024-05-23 14:53:51 +00:00
7d9fde3d1c move old shit
michael pushed to master at school/type-theory 2024-05-23 14:50:48 +00:00
f99ed6bd2b change margins to make the page size more readable
michael pushed to master at school/type-theory 2024-05-23 14:39:17 +00:00
7599cebbf8 concise course in algebraic topology
michael created repository michael/stlc-fstar-proof 2024-05-22 16:12:32 +00:00
michael created branch master in michael/mylang 2024-05-21 09:02:17 +00:00
michael pushed to master at michael/mylang 2024-05-21 09:02:17 +00:00
512f00d53a initial
michael created repository michael/mylang 2024-05-21 09:01:02 +00:00
michael pushed to master at school/type-theory 2024-05-20 21:52:44 +00:00
71b5471d14 progress
michael opened issue school/type-theory#15 2024-05-20 21:51:14 +00:00
Chapter 6: Higher inductive types
michael commented on issue school/type-theory#14 2024-05-20 21:26:16 +00:00
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…

michael opened issue school/type-theory#14 2024-05-20 20:22:40 +00:00
Study Theorem 3.2.2
michael pushed to master at school/type-theory 2024-05-20 08:13:59 +00:00
f0c1bab9ed make sure individual docs render
michael pushed to master at school/type-theory 2024-05-20 08:07:25 +00:00
69350b2242 chapter 3
michael pushed to master at school/type-theory 2024-05-20 07:40:10 +00:00
ce894147d4 progress
michael pushed to master at michael/ddr-scores 2024-05-20 05:02:23 +00:00
0f8fb69e5f delete existing rows
d2979b38ea update 2024-05-19
48c3e45b71 update 2024-05-18
Compare 3 commits »
michael pushed to master at michael/ddr-scores 2024-05-20 05:01:02 +00:00
e8d2f6d031 delete existing rows
d07cf885fe update 2024-05-19
Compare 2 commits »
michael pushed to master at michael/ddr-scores 2024-05-19 21:52:07 +00:00
383e1adf12 update 2024-05-19