Foundations 8: Formal Type Theory and Homotopy Type Theory and Idris
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
https://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 Idris
The idris code used can be found at
https://github.com/richardsouthwell/l...
Please note, the above code is just my attempt to understand
https://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
Watch video Foundations 8: Formal Type Theory and Homotopy Type Theory and Idris online without registration, duration hours minute second in high quality. This video was added by user Richard Southwell 21 February 2021, don't forget to share it with your friends and acquaintances, it has been viewed on our site 5,388 once and liked it 130 people.