Michael Zhang michael
0 followers · 0 following
Repositories
111
 Projects Packages Public activity Starred repositories
michael pushed to master at school/type-theory 2023-05-15 19:18:19 +00:00
9716b4b69b Updates
michael commented on issue school/type-theory#3 2023-05-15 19:17:43 +00:00
Bi-invertible equivalence 
Bool-id : Bool → Bool
Bool-id true = true
Bool-id false = false

Bool-id-pointwise : (b : Bool) → Bool-id (Bool-id b) ≡ b
Bool-id-pointwise true = refl
Bool-id-pointwise false…
michael opened issue school/type-theory#3 2023-05-15 05:35:04 +00:00
Bi-invertible equivalence
michael commented on issue school/type-theory#1 2023-05-14 06:39:11 +00:00
Incorporate reverse-ap for proving equivalence

Ok Favonia's hint is to compute "ap g p", and then concatenate it with a proof that g is the left-inverse of f

Trying with:

Bool-id-inv : Bool → Bool
Bool-id-inv b = (((Bool-id-is-equ…
michael pushed to master at michael/mraow 2023-05-09 20:19:44 +00:00
e78d6ddf99 Chat ...kinda works?
080b4e0e09 Get send message working
d9f08b8deb fix
Compare 3 commits »
michael pushed to master at michael/mraow 2023-05-09 09:43:54 +00:00
b1ef494759 some server work
michael opened issue michael/mraow#2 2023-05-09 09:41:00 +00:00
auth
michael opened issue michael/mraow#1 2023-05-09 09:35:20 +00:00
listen on a port other than 50051
michael pushed to master at michael/mraow 2023-05-09 09:31:52 +00:00
25179a74f7 More UI styling
michael pushed to master at michael/mraow 2023-05-09 09:31:04 +00:00
9bc570db7d More UI styling
michael pushed to master at michael/mraow 2023-05-09 08:15:09 +00:00
87ccab7a4b Update to UI and server
michael pushed to master at michael/mraow 2023-05-09 07:15:17 +00:00
5884bff2c0 Some more web app stuff
10de92a685 Wire up client to talk to server
Compare 2 commits »
michael commented on issue michael/ts-nat-comm#4 2023-05-09 07:13:40 +00:00
shiet

testu

michael pushed to master at school/type-theory 2023-05-09 03:44:08 +00:00
0696c713f7 front matter yml
michael pushed to master at school/type-theory 2023-05-09 02:09:27 +00:00
e71aa3e060 z
michael pushed to master at school/type-theory 2023-05-09 02:09:06 +00:00
bd73915149 z
michael commented on issue school/type-theory#1 2023-05-09 01:59:14 +00:00
Incorporate reverse-ap for proving equivalence

Ok I think I had a slight breakthrough with why I was getting this wrong. I had thought that for a function (f : A -> B) and particular (y : B), the fiber would be (y, f x ≡ y) because of the…

michael closed issue michael/ts-nat-comm#4 2023-05-09 01:31:29 +00:00
shiet
michael closed issue michael/ts-nat-comm#3 2023-05-09 01:31:27 +00:00
ouais
michael closed issue michael/ts-nat-comm#2 2023-05-09 01:31:25 +00:00
test issue