Michael Zhang michael
0 followers · 0 following
Repositories
136
 Projects Packages
5
 Code Public activity Starred repositories
michael created repository michael/cek-call-cc 2024-11-12 07:46:18 +00:00
michael created branch master in michael/tift 2024-11-11 23:35:27 +00:00
michael pushed to master at michael/tift 2024-11-11 23:35:27 +00:00
f617cc8e1c wip
michael created repository michael/tift 2024-11-11 23:35:13 +00:00
michael commented on issue michael/type-theory#23 2024-11-05 10:04:51 +00:00
Understand and define exact sequences

ea7085c26d/src/Misc/FiveLemma/Group/ExactSequence.agda

michael pushed to master at michael/type-theory 2024-11-05 10:04:29 +00:00
ea7085c26d exact sequences
michael closed issue michael/type-theory#46 2024-11-05 09:26:34 +00:00
Prove the five lemma for groups
michael commented on issue michael/type-theory#46 2024-11-05 09:26:08 +00:00
Prove the five lemma for groups

Done! See 90f76baca0/src/Misc/FiveLemma/Group/Lemma.agda for solution

michael closed issue michael/type-theory#48 2024-11-05 09:25:33 +00:00
Five lemma (n is injective)
michael pushed to master at michael/type-theory 2024-11-05 09:25:33 +00:00
90f76baca0 solve the second part too, closes #48
michael commented on issue michael/type-theory#46 2024-11-05 07:20:18 +00:00
Prove the five lemma for groups

Changing this issue to specifically be about groups, will add another one for categories later

michael commented on issue michael/type-theory#47 2024-11-05 07:17:54 +00:00
Five lemma (n is surjective)

Code can be found at 57ce453194/src/Misc/FiveLemma/FiveLemmaGroup.lagda.md (L55)

michael closed issue michael/type-theory#47 2024-11-05 07:16:15 +00:00
Five lemma (n is surjective)
michael pushed to master at michael/type-theory 2024-11-05 07:16:15 +00:00
57ce453194 prove that n is surjective in the five lemma, closes #47
michael opened issue michael/type-theory#48 2024-11-05 07:13:50 +00:00
Five lemma (n is injective)
michael opened issue michael/type-theory#47 2024-11-05 07:13:44 +00:00
Five lemma (n is surjective)
michael commented on issue michael/type-theory#46 2024-11-05 07:10:52 +00:00
Prove the five lemma for groups

Very close to the n surjective result, I defined a different definition of isInIm that isn't truncated: https://git.mzhang.io/michael/type-theory/src/commit/e02f49c46df6d4583bcc1b92f88d733675afc2…

michael commented on issue michael/type-theory#23 2024-11-05 07:08:34 +00:00
Understand and define exact sequences

Started defining this here

michael pushed to master at michael/type-theory 2024-11-05 07:08:20 +00:00
e02f49c46d wip
michael pushed to master at michael/type-theory 2024-11-05 03:26:29 +00:00
fd9f01f914 wip on five lemma and exact sequences