A type theory that can serve as a programming language and as constructive foundations for math proofs.