@ncf@types.pl @mei@donotsta.re @zwarich@hachyderm.io This is why theories like synthetic differential geometry can prove ¬LEM without being paraconsistent, as even though you can prove ¬LEM, you cannot actually construct a closed type A such that ¬(A ∨ ¬A)