"Combines the constructivism of intuitionist logic with the duality of classical logic" sounds interesting. Wish I could read
I found sequent calculus rules online, but I do not understand them. They don't seem like the usual format that typing rules have. I can't really wrap my head around what they're supposed to mean
I wonder if HoTT "scales" to like, analysis and whatnot
Get it. Do you get it. It's cause small step semantics, big step semantics. Do you get it
Someone do this
Or, sneaky anti-LEM
I am like copy, paste, s/blast/iprover, "I am like a mathematician now, probably"
I also hooked up Isabelle's case splitter and induction tactics, but it's anyone's guess whether these actually work cause they rely on classical theorems, and I just lied instead and fed it contrapositivity
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.