3 ms·
LEM for mere propositions is not "true by default", but it is consistent with univalence. So you can take it as an axiom.
by hejsansvejsan 6y ago
LEM for mere propositions is not "true by default", but it is consistent with univalence. So you can take it as an axiom.