Dependent Type Theory: a first approximation
DOI:
https://doi.org/10.15381/pesquimat.v26i1.25523Keywords:
Type Theory, Dependent types, Mathematical foundations, Logic, Proof assistantsAbstract
We present Dependent Type Theory, which combines the concepts of propositions and sets in a more general one, that of “types”. We develop the main notions of this theory, and observe that it can serve as a foundation of mathematics, replacing set theory. We exemplify this studying the natural numbers, and explain how the use of proof assistants gives us a more rigorous foundation for mathematical results.
Downloads
Published
Issue
Section
License
Copyright (c) 2023 Fernando Chu Rivera
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
THE AUTHORS RETAIN THEIR RIGHTS:
a) The authors retain their trademark and patent rights, and also on any process or procedure described in the article.
b) The authors retain the right to share, copy, distribute, execute and publicly communicate the article published in Pesquimat magazine (for example, place it in an institutional repository or publish it in a book), with recognition of its initial publication in the Pesquimat magazine.
c) The authors retain the right to make a later publication of their work, to use the article or any part of it (for example: a compilation of their works, notes for conferences, thesis, or for a book), provided that they indicate the source of publication (authors of the work, magazine, volume, number and date).
