added link to rijkes now published HoTT book
This commit is contained in:
parent
2d33d6dbb7
commit
a1fa31d547
|
@ -149,6 +149,6 @@ If you've made it this far, then congratulations! Even though I've tried to make
|
|||
|
||||
This blog post only covers propositional logic, but one can interpret predicate logic and even higher-order logic within programming languages. This is done with dependent type theory. In dependent type theories, types may themselves *depend* upon values, letting one create types such as `is-even n` which depend on a natural number `n`. This type would have terms which are witnesses that `n` is even. These programming languages, or proof assistants as they are usually called, enable you to prove properties of both programs and mathematical objects. In doing so they provide a way to automatically check mathematical proofs for correctness. There are already many mathematicians using these tools to create formalized proofs of mathematical theorems.
|
||||
|
||||
If you are interested in learning more about dependent type theory, then you might be interested in downloading and playing around with a proof assistant. I recommend [agda](https://agda.readthedocs.io/en/latest/getting-started/installation.html) to those familiar with Haskell; a lengthy [list of agda tutorials](https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html) is included in its documentation. If you wish to learn more about how doing math with types rather than sets might lead to new insights and connections to topology, then I encourage you to learn about homotopy type theory, for which there are some great resources: [HoTTEST Summer School 2022 lectures](https://www.youtube.com/playlist?list=PLtIZ5qxwSNnzpNqfXzJjlHI9yCAzRzKtx), [HoTTEST Summer School 2022 GitHub](https://github.com/martinescardo/HoTTEST-Summer-School), [1lab](https://1lab.dev/1Lab.intro.html), [HoTT Book](https://homotopytypetheory.org/book/), [Egbert Rijkes HoTT intro book](https://github.com/EgbertRijke/HoTT-Intro) (note that this is an older version of Egberts Book, the final version is expected to be published soon).
|
||||
If you are interested in learning more about dependent type theory, then you might be interested in downloading and playing around with a proof assistant. I recommend [agda](https://agda.readthedocs.io/en/latest/getting-started/installation.html) to those familiar with Haskell; a lengthy [list of agda tutorials](https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html) is included in its documentation. If you wish to learn more about how doing math with types rather than sets might lead to new insights and connections to topology, then I encourage you to learn about homotopy type theory, for which there are some great resources: [HoTTEST Summer School 2022 lectures](https://www.youtube.com/playlist?list=PLtIZ5qxwSNnzpNqfXzJjlHI9yCAzRzKtx), [HoTTEST Summer School 2022 GitHub](https://github.com/martinescardo/HoTTEST-Summer-School), [Introduction to Homotopy Type Theory](https://arxiv.org/abs/2212.11082), [1lab](https://1lab.dev/1Lab.intro.html), [HoTT Book](https://homotopytypetheory.org/book/).
|
||||
|
||||
{% endkatexmm %}
|
||||
|
|
Loading…
Reference in New Issue
Block a user