Meven Lennon-BertrandRE: https://mathstodon.xyz/@markusde/116020715195099414
Oh boy, I've been *asked* to rant about constructivity and Lean's type theory, so here I come. Beware, long thread incoming (I tried to keep it reasonable, I have definitely failed).
chris martens@mevenlennonbertrand one of my favorite things in the world is when a person who’s deeply curious about a topic but shy about asking and someone who’s itching to infodump about that topic but thinks no one will care, find out that each other exist