Foundations 8: Formal Type Theory and Homotopy Type Theory and Idris
ฝัง
- เผยแพร่เมื่อ 20 ก.พ. 2021
- 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 the formal rules for the intensional dependent type theory described in
homotopytypetheory.org/book/
We also provide look at a brief introduction to homotopy type theory, by describing the additional axioms (functional extensionality and the univalence axiom), which need to be added to the dependent type theory we have described to form homotopy type theory.
A description of how to implement category theory with the Idris programming language can be found here:
• Category Theory With I...
The idris code used can be found at
github.com/richardsouthwell/l...
Please note, the above code is just my attempt to understand
github.com/statebox/idris-ct
Videos describing how to install idris and vscode (patience required !) can be found here:
• Installing Idris 1
• Installing Idris 2
• Installing Idris 3
It was when I started to learn type theory that I found your videos. It took me a week to study this series and now I have got a high level overview of this subject. Now I am quite confident to go on, and thank you very much! Appreciate your effort!
this has been my favourite video in the series. It's really good!
Really enjoyable series. Thank you!
This series is great! Are you planning on doing a video on lambda calculus?
I haven't checked and this was 8 months ago, but if you wanted he's simple type theory probably goes over it a little bit
Hello Richard!
May you recommend a good introductory books on the foundations of mathematics:
I.e: Logic, Sets, and Numbers
Something for Beginners!!
Thank you
6 months ago Richard sent a post on this channel named "One Milon view special - My favorite Books"
@@polacy_w_strefie_komfortu I found it, thank you!
@@HaCkeMatician Yep that is correct. If starting from nothing I would recommend `Concepts of Modern Mathematics' (Stewart), then `Conceptual Mathematics' (Lawvere), then maybe the homotopy type theory book, or Mclarty's category theory/topos book (depending upon what you are into after reading the first two). Good luck !
@@RichardSouthwell
Thank you, Richard!
Really appreciate it!
Have a nice day.
@@RichardSouthwell Is there a book(or multiple books) that's considered gold standard for learning all the logic necessary in type theory that is used in different papers on gradual types, dependent types?
Thank you!
Hi, Richard, I am currently at video 3 of this series. Is this series completed?
yes, 8 is the last video on this playlist th-cam.com/play/PLCTMeyjMKRkqTM2-9HXH81tvpdROs-nz3.html and that completes the series
@@RichardSouthwell thanks for putting the time in and making it available, you are doing special work.
At 1:31:00, you seem to be saying type theory is more fundamental than numbers because the infinite nature of numbers is difficult to represent. But aren’t types also infinite because Ui:U_i+1? Moreover, aren’t you already relying on numbers to describe this type hierarchy?
His statements there are in reference to the distinction between potential infinity versus actual infinity where the former is thought of as an indefinitely extendable process or concept in which infinity is implied and the latter is thought of as something given in its infinite form a priori. The type hierarchy is an example of a potential infinity where as the Natural Numbers as a type is an example of an actual infinity (the natural numbers must exist before you can say something is of that type and because there are infinitely many of them then they must represent an actual infinity). The concept of actual infinity has historically, and continues to be, a controversial idea in mathematics. Here I believe Southwell is stating that he doesn't believe that actual infinity is a legitimate concept because of the difficulties he finds in incorporating the Natural Number Type into Type Theory.