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
www.math.mcgill.ca/rags/LCCC/...
More on topos theory can be found here
• Category Theory For Be...

[@RichardSouthwell]

The final video in this course (unless I decide to extend) will be released in two weeks !

[@jontedeakin1986]

what else would there be to mention? it seemed to me that the point of the series was to build to htt.

[@Andrew-rc3vh]

I just jumped straight in to this one. Still it seemed to make sense to me. Being a programmer, these concepts feel familiar. it's testament to the clear way it is explained that you can jump straight in and still get it. Thanks.

[@dr.c2195]

I like the change in presentation style. What you write is easier to read this way.
Also, I like the idea of Σ and Π types a lot. I was reading a book that is entitled "Type Theory & Functional Programming" and so far (I have not read all of it yet) it only talks about the logic interpretation of ∃ and ∀. What I like about the Σ and Π types is that it causes writing types as A^B to make a lot sense. A^B is just A multiplied with itself B times, and that is also what Π(a:A)B does when B does not depend on A.
The Ε and Π types also make it seem like maybe this pattern could be continued as well, where you e.g. have Ε(a:A)B which would be repeated exponentiation (Ε is epsilon for exponentiation). And if B is constant then you get A^^B (tetration). And then you can do Τ(a:A)B, for repeated tetration (Τ is tau for tetration), etc.

[@behnamplays]

Interesting to see the use of iPad in your lectures! I like both blackboard and iPad styles. Keep up the good work!

[@tanchienhao]

amazing video series! thank you :)

[@jontedeakin1986]

Holy moly, this series has been the biggest help. Thank you so much for making it!!!

[@zacharybanken7355]

Thanks! This helped me understand dependent type theory in Lean better

[@rikkertkoppes]

The number of ads in the first hour is through the roof. Is this intentional?
Furthermore, recently heard about Poly from Spivak, but his lectures assume quite a lot of upfront knowledge, which I don't have. Seems like a very interesting, but also down to earth, subject to me. Might this be an idea for a next series?

[@mayabartolabac]

what is this Poly from Spivak about?

[@rikkertkoppes]

@@mayabartolabac th-cam.com/video/Cp5_o2lDqj0/w-d-xo.html

[@mayabartolabac]

@@rikkertkoppes reading the description already intrigues me

[@cynocephalusw]

Great job!

[@piglava]

Absolute legend