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).
Martin EscardoGreat thread.
So many things I agree and disagree with!
But let me address the (dis)agreements another time.
@MartinEscardo Very curious to hear about that!