
TL;DR
This paper explores the evolution of mathematical concepts like truth and equality, emphasizing recent advances in dependent type theory and infinity categories, highlighting their implications for mathematics and computer science.
Contribution
It provides a historical overview and discusses recent developments in dependent type theory and homotopy type theory, illustrating their significance for foundational mathematics and computer science.
Findings
Dependent type theory enables new ways to handle equality and isomorphisms.
Homotopy type theory offers a unifying framework connecting logic, topology, and category theory.
These theories support computer-assisted proofs and software verification.
Abstract
This text summarizes and expands the content of a general audience talk given in 2018 at the University of Mainz. Motivated by recent developments in dependent type theory and infinity category theory, it presents a history of ideas around the concepts of truth, proof, equality, and equivalence as well as their relation to human thought. We describe a few selected ideas of Platon, Aristoteles, Leibniz, Kant, Frege and others and then pass to the results of G\"odel and Tarski about incompleteness, undecidability and truth in deductive systems and their semantic models. The main focus of this text, however, is the development of dependent type theory through the work of Per Martin--L\"of and recent developments in homotopy type theory, i.e., the univalent foundations program of Vladimir Voevodsky and others. These theories allow the notion of identity types, which gives new possibilities…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
