Michael Zhang michael
0 followers · 0 following
Repositories
123
 Projects Packages Code Public activity Starred repositories
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
michael pushed to master at school/type-theory 2023-05-17 04:13:15 +00:00
9e1d8d57ba 2.3 lemmas
michael pushed to master at school/type-theory 2023-05-17 03:23:40 +00:00
c7276238b2 add hott book files
michael commented on issue school/type-theory#6 2023-05-16 16:59:47 +00:00
Exercise 2.4: n-dimensional path

Just putting some old attempts here:

-- data nPath {A : Type} : ℕ → Type where                          
--   zeroPath : (x y : A) → (p : x ≡ y) → nPath zero              …
michael pushed to master at school/type-theory 2023-05-16 14:38:52 +00:00
a8a53ddc21 readme
michael opened issue school/type-theory#7 2023-05-16 14:05:07 +00:00
Chapter 2
michael opened issue school/type-theory#6 2023-05-15 23:27:47 +00:00
N dimensional path (2.4)
michael opened issue school/type-theory#5 2023-05-15 19:36:39 +00:00
Port cohomology paper to cubical Agda
michael opened issue school/type-theory#4 2023-05-15 19:34:26 +00:00
Write a blog post for the fundamental group of a circle ≡ integers
michael commented on issue school/type-theory#2 2023-05-15 19:33:46 +00:00
Path between fibers for boolean equivalence

Trying this again in this file

I feel like the answer here was I'm trying to make fx and fz ≡…

michael commented on issue school/type-theory#1 2023-05-15 19:31:00 +00:00
Incorporate reverse-ap for proving equivalence

I think I got the idea, see this file

eqv5 : convert-inv (convert z) ≡ convert-inv (convert…
michael closed issue school/type-theory#1 2023-05-15 19:31:00 +00:00
Incorporate reverse-ap for proving equivalence
michael pushed to master at school/type-theory 2023-05-15 19:29:49 +00:00
f34cb844a4 hmm
michael commented on issue school/type-theory#3 2023-05-15 19:19:19 +00:00
Bi-invertible equivalence

I think this is resolved in 9716b4b69b3af70dcab68ed3d5321adb8789dfbd ?

reason for i think is because the Iso doesn't actually use the BiInvEquiv itself, but i think that's fine for now

michael closed issue school/type-theory#3 2023-05-15 19:19:19 +00:00
Bi-invertible equivalence