pounce @pounce@types.pl
i like topology, tea and type theory
Joined Dec 2020
also:
I think the heart of free software is really great!! It's just... some of the people....
postdoc im reading HoTT with: the best way to connect with other mathematicians outside of school is to make a math twitter
nooooooo
tfw forgot how to homotopy theory when doing homotopy type theory
aaaaa why is the only wikipedia citation to this a website from 2003 archived in the wayback machine with all the links to proofs broken
logic thonk
ok, so set theory relies heavily on second-order logic to function, and second-order logic/set theory are two main levels on top of which most of mathematics is built, right?
i see type theory as championed by not having this hierarchy by "properties-as-types", however all the type theories i've seen have "judgements" of typing rules and equality that dictate how the type theory function. Is this not also a "two-level hierarchy" on which type theory is built? or am i thinking about the relationship wrong
me: Julia what's typeof(f)
Julia: typeof(f)
me:.... yes that's what i asked
ok while we're talking about go can i complain about how long it takes `vim-go` to update all of its binaries when every other plugin updates instantly
for a language that prides itself on fast compile time it's pretty sad
pounce
boosted
if you need to design an entire templating tool for a language solely to work around its shortcomings or eliminate boilerplate, your language sucks
i am so tired of listening to people designing tools to clean up after Go's failings
ayyy my alpha beta search works on the first time
i win against the executable they gave us 77% of the time
why does it figure out judgemental equality for lambdas but not functions in `where` blocks
grrr why is the lean typechecker so dumb
consumerism
i kinda want a tablet to take notes on since i keep using my partner's during calls
is that a bad idea 
i have just. done my third talk on lean
i don't even use lean for any reason except it's somewhat easier to write fast code in than agda
why do ppl keep asking me to talk about it 🙃
maybe if i make some hōjicha i'll finally be able to read that Escardó paper that's been sitting on my bedside table since december
i feel like i need to make one of those "we have been played for absolute fools" memes about category theory
HoTT exercises
hmmm
2.1/2.2 is kinda getting me. So I have to prove equality of these three proofs using path-induction
but clearly they don't use path induction in the same way, so they aren't judgmentally equal.
But each of these are functions, so don't I need funext to prove non-judgmentally-equal functions as equal?
i like topology, tea and type theory
Joined Dec 2020
