3 ms·
> An interesting example is the Axiom of Choice which is, naively encoded, a theorem of intuitionistic logic. Naïvely encoded in Martin-Löf type theory, that i
by catnaroek 11y ago
> An interesting example is the Axiom of Choice which is, naively encoded, a theorem of intuitionistic logic.
Naïvely encoded in Martin-Löf type theory, that is.