Foundations 6: Simple Type Theory

In this series we develop an understanding of the modern foundations of pure mathematics, starting from first principles. We start with intuitive ideas about set theory, and introduce notions from category theory, logic and type theory, until we are in a position to understand dependent type theory, and in particular, homotopy type theory, which promises to replace set theory as the foundation of modern mathematics. We also take an interest in computer science, and how to write computer programming languages to formalize mathematics. In this video we describe simple type theory, which is also known as typed lambda calculus with sums. This is a formal theory which can be used to describe set theory, intuitionistic logic, and any other cartesian closed category. We explain all the inference rules for the simple type theory, and describe how they relate to familiar ideas from category theory. We also practically demonstrate how to form a programming language implementing the rules, using Javascrip