Michael Zhang michael
0 followers · 0 following
Repositories
123
 Projects Packages Code Public activity Starred repositories
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 pushed to master at michael/mylang 2024-05-21 09:02:17 +00:00
512f00d53a initial
michael created branch master in michael/mylang 2024-05-21 09:02:17 +00:00
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
michael pushed to master at school/type-theory 2024-05-18 00:35:51 +00:00
8658b6a2f5 exercise
michael pushed to master at school/type-theory 2024-05-17 23:35:19 +00:00
f9ee8c0503 update
michael pushed to master at school/type-theory 2024-05-17 22:37:28 +00:00
447bd52025 update
michael pushed to master at school/type-theory 2024-05-17 18:50:51 +00:00
87ab99506c progress
michael pushed to master at school/type-theory 2024-05-17 06:49:15 +00:00
5c35f42baf compile