3 ms·
The untyped lambda calculus is inconsistent as a logic, hence you need some notion of types. Type theory is indeed building mathematics from lambdas, though.
by carnitine 5y ago
The untyped lambda calculus is inconsistent as a logic, hence you need some notion of types.
Type theory is indeed building mathematics from lambdas, though.
- bsedlm 5y agobecause of the y-combinator|russell paradox? correct?? better question: any references to a type-based construction of set theory?
- anchpop 5y agoYou should read the homotopy type theory book if you’re interesting in things like this :p But to answer your question, there’s one here: https://arxiv.org/abs/1305.3835 https://arxiv.org/abs/1305.3835