💾 Archived View for gemlog.blue › users › jiaming › 1630354938.gmi captured on 2024-03-21 at 18:37:18. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2021-12-04)
-=-=-=-=-=-=-
30/08/2021 (things i learned)
- HoTT lectures!!! Super mesmerizing
- They are a great supplement the HoTT textbook. (will it be vital? maybe for motivation?)
- Andrej Bauer, Egbert Rijke, ... some more who else to look out for for TT material
- good for programming language creators? I should take a look
Programming Language Zoo (by Andrej Bauer & Matija Pretnar)
- Thanks to mathlib porting, i know just the word needed for i18n of existing PLs. PORT
- cant wait for 2021's one, i dont like the poster-y format tho
- AAC is the most popular audio compression codec
- i need to dig into container formats
- Slavic, Germanic and Romance European language categorization (my lack of hatred towards english language despite betrayal is quite revealing about my own kolomentality/colomentality/kolomentaliti/kolomentaliti/colonial mentality)
- Ohh english is germanic with lots of romance vocab influence (or creolized??)
- ummmm........ how to go back to Lean 3 .. ....
- Hmm btw interesting how i learn about countries now.. First question is who colonized it? (i probably alr know if its a colonizer country) and when? Ohh Slovenia during WW2 by various ppl surrounding, understandable (and funny)
- I'll be honest, WW2 in europe was hilarious. In asia not so much. But cold war is some dark times
- You Mean The World To Me 2017 penang hokkien movie trailer
- veritasium is so so so colonizer yikes not even self-aware
- i wonder how to do a search for string with set hammed (hamming yuck) distance
- DONT LOSE TO TIKTOK ya allah i thought i was better than this, tho an archive spree is settling in soon i can feel it
- omg polish flag is so offensive
Super handy IPA pronunciation guide
- According to wikipedia and wikitionary, it's /məˈleɪziə, -ʒə/ ohhh if you hover with mouse it'll give an example! how useful
- ohh scientific socialism just means evidence based & learning from history i guess. not the PAS kind xD
https://activism.openworlds.info/@jiaming/106846886350999179
- ishhh the indonesian flag icon doesnt appear on lynx/terminal/console. just says ID ughhh
- OK im in love with mastodon tho, good accessibility good design & scrapable/archivable, no evil LOGIN B*TCH pop ups which ive been battered into getting used to :(
- also... I HAVE 42 FOLLOWERS?? Since when omg ahhaa
- Server side Advertisement Insertion... [[Server-Side Ad Insertion (SSAI)]] cancer
- square nails as a natural breaking phenomenon?
- btw f*ck replacement classes & exams
- How to construct the type `ind : Π(C:ℕ→U). C(0) → (Π(n:ℕ). C(n) → C(succ n)) → Π(n:ℕ). C(n)`? Based off of their definitional equations?
hmm look! `def swap : Π(A B C:U). (A → B → C) → B → A → C := λA B C. λg. (λb. λa. g a b)` (ok im not sure if lambdas can have same names as their Pi's. but u get the idea)
- Just create lambdas to match their definitional equations?
- Hmm the recursor for boolean types looks like it needs some ORs or case splittings to define! cuz got two definitional equations
- So.. since natural number induction also has two definitional equations... WE PROBABLY NEED CASE SPLITTING TOO!
- You f-ing skimmed sums and co-products ugh, read through again ull probably get it now