An introduction to type theory and the univalence axiom, aimed at advanced undergraduate and graduate students of mathematics and computer science with an interest in the foundations and formalization of mathematics. Prerequisites are minimal and over 200 exercises provide ample practice material.
An introduction to type theory and the univalence axiom, aimed at advanced undergraduate and graduate students of mathematics and computer science with an interest in the foundations and formalization of mathematics. Prerequisites are minimal and over 200 exercises provide ample practice material.
Egbert Rijke is Postdoctoral Research Fellow at Johns Hopkins University and is a pioneering figure in homotopy type theory. As one of the co-authors of the influential book 'Homotopy Type Theory: Univalent Foundations of Mathematics' (2013), he has played a pivotal role in shaping the field. He is also a founder and lead developer of the agda-unimath library, which stands as the largest library of formalized mathematics written in the Agda proof assistant.
Inhaltsangabe
Preface Introduction Part I. Martin-Löf's Dependent Type Theory: 1. Dependent type theory 2. Dependent function types 3. The natural numbers 4. More inductive types 5. Identity types 6. Universes 7. Modular arithmetic via the Curry-Howard interpretation 8. Decidability in elementary number theory Part II. The Univalent Foundations of Mathematics: 9. Equivalences 10. Contractible types and contractible maps 11. The fundamental theorem of identity types 12. Propositions, sets, and the higher truncation levels 13. Function extensionality 14. Propositional truncations 15. Image factorizations 16. Finite types 17. The univalence axiom 18. Set quotients 19. Groups in univalent mathematics 20. General inductive types Part III. The Circle: 21. The circle 22. The universal cover of the circle References Index.
Preface Introduction Part I. Martin-Löf's Dependent Type Theory: 1. Dependent type theory 2. Dependent function types 3. The natural numbers 4. More inductive types 5. Identity types 6. Universes 7. Modular arithmetic via the Curry-Howard interpretation 8. Decidability in elementary number theory Part II. The Univalent Foundations of Mathematics: 9. Equivalences 10. Contractible types and contractible maps 11. The fundamental theorem of identity types 12. Propositions, sets, and the higher truncation levels 13. Function extensionality 14. Propositional truncations 15. Image factorizations 16. Finite types 17. The univalence axiom 18. Set quotients 19. Groups in univalent mathematics 20. General inductive types Part III. The Circle: 21. The circle 22. The universal cover of the circle References Index.
Es gelten unsere Allgemeinen Geschäftsbedingungen: www.buecher.de/agb
Impressum
www.buecher.de ist ein Internetauftritt der buecher.de internetstores GmbH
Geschäftsführung: Monica Sawhney | Roland Kölbl | Günter Hilger
Sitz der Gesellschaft: Batheyer Straße 115 - 117, 58099 Hagen
Postanschrift: Bürgermeister-Wegele-Str. 12, 86167 Augsburg
Amtsgericht Hagen HRB 13257
Steuernummer: 321/5800/1497
USt-IdNr: DE450055826
