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 Javascript.
A theory close to the one we describe is given in the paper:
Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums, Balat,Cosmo,Fiore
https://www.cl.cam.ac.uk/~mpf23/paper...
I wrote the following document which describes the simple type theory and how it gives rise to constructions with universal properties in category theory:
https://github.com/AviCraimer/type-th...
The computer code we mentioned for implementing simple type theory can be found here:
https://github.com/AviCraimer/type-th...
https://github.com/AviCraimer/type-th...
Additional information about how to justify the universality of coproducts in this simple type theory can be found in these videos:
• MF 6 10
• MF 6 11
• MFOM 6 12
• MF 6 alpha conversion
Watch video Foundations 6: Simple Type Theory online without registration, duration hours minute second in high quality. This video was added by user Richard Southwell 25 January 2021, don't forget to share it with your friends and acquaintances, it has been viewed on our site 7,133 once and liked it 180 people.