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