Michael Zhang michael
michael created repository osu/spelunker 2023-05-19 22:33:15 +00:00
michael pushed to master at michael/fastdoc 2023-05-18 20:25:30 +00:00
michael pushed to master at michael/fastdoc 2023-05-18 18:54:08 +00:00
b5760b09a5 Walk
michael pushed to master at michael/fastdoc 2023-05-18 18:32:50 +00:00
8371167ee3 Fastdoc
michael created branch master in michael/fastdoc 2023-05-18 18:32:50 +00:00
michael created repository michael/fastdoc 2023-05-18 18:32:38 +00:00
michael pushed to master at school/type-theory 2023-05-18 08:28:22 +00:00
6d0e500a59 updates
michael opened issue school/type-theory#10 2023-05-18 08:27:33 +00:00
Exercise 4.6: qinv-univalence
michael pushed to master at school/type-theory 2023-05-18 05:43:01 +00:00
c7f4ee0708 idk what this progress was but here's progress
michael opened issue school/type-theory#9 2023-05-18 05:40:39 +00:00
Chapter 3: Sets and logic
michael pushed to master at michael/openstellaris 2023-05-18 05:14:55 +00:00
4d89c97ec9 vite
michael pushed to master at michael/openstellaris 2023-05-18 05:13:09 +00:00
michael pushed to master at school/type-theory 2023-05-17 09:53:16 +00:00
3c668bfd02 wip 2.13
michael opened issue school/type-theory#8 2023-05-17 09:52:17 +00:00
Exercise 2.13: (2 ≃ 2) ≃ 2
michael pushed to master at school/type-theory 2023-05-17 09:01:14 +00:00
98c5b14e06 stuck again
michael commented on issue school/type-theory#2 2023-05-17 09:00:21 +00:00
Path between fibers for boolean equivalence

ok going to try this again without cubical in this doc

using path induction, I was able…

michael pushed to master at school/type-theory 2023-05-17 08:20:43 +00:00
ae0452715b port to non cubical hott
michael pushed to master at school/type-theory 2023-05-17 08:02:49 +00:00
1368b9e2c9 ch 6
michael pushed to master at school/type-theory 2023-05-17 06:28:35 +00:00
1a3828bbaa some more shit
michael pushed to master at school/type-theory 2023-05-17 04:31:39 +00:00
afb49b5b35 rest of 2.3