[Ed.] C.B. has provided a much better typeset PDF version of this blog post. Dependent types are ubiquitous in mathematics, pure and applied. When we say “let be a vector of length ,” we make the collection of values to which may belong dependent upon the value of . Such dependency of types-of-things on values-of-things is fundamental to our ability to express complex mathematical ideas and build up sophisticated abstractions. By taking this essential idea to heart, dependent type theory ...
