Foundations 7: Dependent 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 introduce the concepts of dependent type theory (intensional Martin-Löf' type theory). In particular, we introduce type families, sigma types, pi types, identity types, propositional and judgmental equality, and natural number types. We also describe how dependent type theory relates to the theory of slice categories for locally Cartesian closed categories.
The following paper describes this theory in more detail:
R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95
https://www.math.mcgill.ca/rags/LCCC/...
More on topos theory can be found here
• Category Theory For Beginners: Topos ...
Смотрите видео Foundations 7: Dependent Type Theory онлайн без регистрации, длительностью часов минут секунд в хорошем качестве. Это видео добавил пользователь Richard Southwell 07 Февраль 2021, не забудьте поделиться им ссылкой с друзьями и знакомыми, на нашем сайте его посмотрели 7,767 раз и оно понравилось 168 людям.