Introduction to Homotopy Type Theory

📘 مقدمه‌ای به نظریه نوع و نظریه نوع هموتوپی

📚 این معرفی به‌روز از نظریه نوع و نظریه نوع هموتوپی، مطالعه‌ای ضروری برای دانشجویان کارشناسی پیشرفته و تحصیلات تکمیلی است که به بنیان‌ها و صورت‌بندی صوری ریاضیات علاقه‌مند هستند.

📘 کتاب با یک مقدمهٔ کامل و خودبسنده بر نظریه نوع وابسته آغاز می‌شود. هیچ پیش‌نیاز قبلی از نظریه نوع لازم نیست. بخش دوم به‌تدریج مفاهیم کلیدی نظریه نوع هموتوپی را معرفی می‌کند: هم‌ارزی‌ها، قضیهٔ بنیادی انواع هویت، سطوح تراکمی و اصل یکنواختی (Univalence Axiom). این مباحث خواننده را برای مطالعهٔ موضوعات مختلف از دیدگاه یکپارچه (univalent) آماده می‌کند، از جمله مجموعه‌ها، گروه‌ها، ترکیبیات و درخت‌های خوش‌بنیاد. بخش پایانی نیز مفهوم انواع استقرایی مرتبه‌بالا را با بررسی دایره و پوشش جهانی آن معرفی می‌کند. هر بخش به فصل‌هایی کوتاه در حد یک جلسهٔ درسی تقسیم شده و بیش از ۲۰۰ تمرین برای تثبیت مفاهیم ارائه شده است.

📑 فهرست مطالب

بخش 1: نظریه نوع وابسته مارتین-لف

فصل 1: نظریه نوع وابسته

فصل 2: انواع تابع وابسته

فصل 3: اعداد طبیعی

فصل 4: انواع استقرایی بیشتر

فصل 5: انواع هویت

فصل 6: جهان‌ها

فصل 7: حساب پیمانه‌ای از طریق تفسیر کاری–هاوارد

فصل 8: تصمیم‌پذیری در نظریه مقدماتی اعداد

بخش 2: بنیان‌های یکنواخت ریاضیات

فصل 9: هم‌ارزی‌ها

فصل 10: انواع تراکم‌پذیر و نگاشت‌های تراکم‌پذیر

فصل 11: قضیهٔ بنیادی انواع هویت

فصل 12: گزاره‌ها، مجموعه‌ها و سطوح تراکمی بالاتر

فصل 13: گستردگی تابعی

فصل 14: تراکم‌های گزاره‌ای

فصل 15: تجزیه تصویر (Image Factorization)

فصل 16: انواع متناهی

فصل 17: اصل یکنواختی

فصل 18: خارج‌قسمت‌های مجموعه‌ای

فصل 19: گروه‌ها در ریاضیات یکنواخت

فصل 20: انواع استقرایی عمومی

بخش 3: دایره

فصل 21: دایره

فصل 22: پوشش جهانی دایره

📚 نقد و بررسی

📘 «رویای ریاضی‌دان برای شناسایی اشیائی که معادل‌اند، یکی از اصل‌های بنیادین نظریهٔ نوع هموتوپی است؛ نظریه‌ای که اصل یکنواختی وویودسکی را با تفسیر هموتوپیکی از نظریهٔ نوع وابستهٔ مارتین-لف ترکیب می‌کند. ریکه یک مقدمهٔ زیبا ارائه کرده که این بنیان‌های یکنواختی را از حالت رازآلود خارج می‌کند و با مجموعه‌ای گزیده از مثال‌ها و تمرین‌ها، تازه‌واردان را قادر می‌سازد به‌سرعت شهود لازم برای نوشتن برهان‌های خود—چه روی کاغذ و چه با نرم‌افزارهای اثبات خودکار—را به‌دست آورند.»

— امیلی ریل، دانشگاه جانز هاپکینز

📘 «کتاب اصلی HoTT در IAS به‌عنوان یک آزمایش نوشته شد و دقیقاً هم چنین به نظر می‌رسد. اکنون زمان آن رسیده که یک مقدمهٔ بالغ، منسجم و آموزشی برای این حوزهٔ انقلابی داشته باشیم؛ حوزه‌ای که نظریهٔ هموتوپی، نظریهٔ نوع سازنده و نظریهٔ رده‌های بالاتر را ترکیب می‌کند. اگبرت ریکه دقیقاً چنین کتابی را ارائه داده است.»

— استیو اوودی، دانشگاه کارنگی ملون

📘 «نظریهٔ نوع هموتوپی حوزه‌ای جدید و به‌سرعت در حال تحول است و تاکنون کتاب درسی به‌روز و قابل‌دسترسی برای دانشجویان نداشته است. ریکه که خود از مشارکت‌کنندگان اصلی این حوزه است، کتابی عالی نوشته که از مبانی آغاز می‌کند، بدون فرض پیش‌زمینه در نظریه نوع، و تا اصل یکنواختی، انواع استقرایی مرتبه‌بالا و ایده‌های اصلی هموتوپی ترکیبی پیش می‌رود.»

— مایک شولمن، دانشگاه سن‌دیگو

📘 «کتاب اگبرت ریکه یک مقدمهٔ دوستانه به نظریهٔ نوع هموتوپی است؛ نظامی صوری برای بنیان جدید ریاضیات که به‌جای نظریهٔ مجموعه‌ها بر نظریهٔ نوع تکیه دارد. در بخش اول، نظریهٔ نوع مارتین-لف ارائه می‌شود و در بخش دوم با افزودن اصل یکنواختی و انواع استقرایی عمومی، HoTT معرفی می‌گردد. فصل پایانی به ساخت و بررسی “دایرهٔ منطقی” اختصاص دارد. این توسعه ریشه در تفسیر توپولوژیکی نظریه نوع مارتین-لف دارد که توسط اوودی-وارن و وویودسکی مطرح شد. اگرچه این تفسیر در کتاب کمتر توضیح داده شده و ممکن است برای خواننده شگفت‌انگیز باشد، اما مطالعهٔ کتاب درک من از HoTT را به‌طور قابل توجهی بهبود داد. تمرین‌های خوبی در کتاب وجود دارد و دایرهٔ منطقی فصل آخر یک کاربرد انقلابی است.»

— آندره ژوآل، دانشگاه کبک در مونترآل

👤 درباره نویسنده

📚 اگبرت ریکه پژوهشگر پسادکتری در دانشگاه جانز هاپکینز است و از چهره‌های پیشگام در نظریه نوع هموتوپی محسوب می‌شود. او یکی از نویسندگان کتاب تأثیرگذار Homotopy Type Theory: Univalent Foundations of Mathematics است و نقش مهمی در شکل‌گیری این حوزه داشته است. همچنین او بنیان‌گذار و توسعه‌دهندهٔ اصلی کتابخانهٔ agdaunimath است که بزرگ‌ترین کتابخانهٔ ریاضیات صورت‌بندی‌شده در سیستم اثبات‌گر آگدا به شمار می‌رود.

This up-to-date introduction to type theory and homotopy type theory will be essential reading for advanced undergraduate and graduate students interested in the foundations and formalization of mathematics.

The book begins with a thorough and self-contained introduction to dependent type theory. No prior knowledge of type theory is required. The second part gradually introduces the key concepts of homotopy type theory: equivalences, the fundamental theorem of identity types, truncation levels, and the univalence axiom. This prepares the reader to study a variety of subjects from a univalent point of view, including sets, groups, combinatorics, and well-founded trees. The fnal part introduces the idea of higher inductive type by discussing the circle and its universal cover. Each part is structured into bite-size chapters, each the length of a lecture, and over 200 exercises provide ample practice material.

Table of Contents

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

Review

‘The mathematician’s dream of identifying objects that are equivalent is a foundational axiom of Homotopy Type Theory, which combines Voevodsky’s univalence axiom with a homotopical interpretation of Martin-Löf’s dependent type theory. Rijke has produced a beautiful introduction that demystifies these univalence foundations, with a curated list of examples and exercises that enable newcomers to rapidly develop the intuitions necessary to learn how to write their own proofs, either on paper or with a computer proof assistant.’ Emily Riehl, Johns Hopkins University

‘The original HoTT Book was written at the IAS as an experiment – and reads like it. It is high time for a mature, uniform, pedagogical introduction to this revolutionary field, which combines homotopy theory, constructive type theory, and higher category theory. Egbert Rijke has given us just such a book.’ Steve Awodey, Carnegie Mellon University

‘Homotopy type theory is a new and rapidly changing field, and until now there have been no up-to-date textbooks accessible to students. Rijke, himself a major contributor to the subject, has produced an excellent book that starts from the basics, assuming no background in type theory, and leads up to the univalence axiom, higher inductive types, and the basic ideas of synthetic homotopy theory. This book should be valuable to anyone wanting to get involved in this new and exciting area.’ Mike Shulman, University of San Diego

‘The book of Egbert Rijke is a friendly introduction to Homotopy Type Theory (HoTT), a formal system for a new foundation of mathematics based on type theory, instead of set theory. Martin-Löf Type Theory (MLTT) is presented in the first part of the book, and HoTT in the second part by adding Voevodsky’s univalence axiom and general inductive types. The last chapter is devoted to the construction and study of the logical circle. The development of HoTT can be traced back to the discovery of the topological interpretation of MLTT by Awodey-Warren and Voevodsky. But the fact that this interpretation is seldom discussed in the book can be surprising to the reader. But I confess that my understanding of HoTT was greatly improved by reading the book as it stands. It contains a set of well-chosen exercises. The logical circle in the last chapter is a revolutionary application.’ André Joyal, Université du Québec à Montréal

About the Author

Egbert Rijke is Postdoctoral Research Fellow at Johns Hopkins University and is a pioneering fgure in homotopy type theory. As one of the co-authors of the infuential book Homotopy Type Theory: Univalent Foundations of Mathematics, he has played a pivotal role in shaping the feld. He is also a founder and lead developer of the agdaunimath library, which stands as the largest library of formalized mathematics written in the Agda proof assistant.