Hacker News Reader

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.

because of the y-combinator|russell paradox? correct??

better question: any references to a type-based construction of set theory?

You 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