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

http://math.andrej.com/

- 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

Bitmovin 2020 Surveyyyy

- 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

Train of thought to understand ind and rec (induction and recursion)

- 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