Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv
@ 2022-12-23  9:54 Egbert Rijke
  2022-12-23 14:22 ` João Alves Silva Júnior
                   ` (2 more replies)
  0 siblings, 3 replies; 6+ messages in thread
From: Egbert Rijke @ 2022-12-23  9:54 UTC (permalink / raw)
  To: Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 1900 bytes --]

Dear homotopy type theorists,

My textbook Introduction to Homotopy Type Theory is finished and available
on the ArXiv:

https://arxiv.org/abs/2212.11082

From the abstract:
This is an introductory textbook to univalent mathematics and homotopy type
theory, a mathematical foundation that takes advantage of the structural
nature of mathematical definitions and constructions. It is common in
mathematical practice to consider equivalent objects to be the same, for
example, to identify isomorphic groups. In set theory it is not possible to
make this common practice formal. For example, there are as many distinct
trivial groups in set theory as there are distinct singleton sets. Type
theory, on the other hand, takes a more structural approach to the
foundations of mathematics that accommodates the univalence axiom. This,
however, requires us to rethink what it means for two objects to be equal.
This textbook introduces the reader to Martin-Löf's dependent type theory,
to the central concepts of univalent mathematics, and shows the reader how
to do mathematics from a univalent point of view. Over 200 exercises are
included to train the reader in type theoretic reasoning. The book is
entirely self-contained, and in particular no prior familiarity with type
theory or homotopy theory is assumed.

Over Christmas I will write a blog post in which I will go more into the
content of the book. For now: Enjoy!

Happy holidays to everyone!
Egbert

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 2311 bytes --]

^ permalink raw reply	[flat|nested] 6+ messages in thread

end of thread, other threads:[~2023-01-13 14:55 UTC | newest]

Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-12-23  9:54 [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv Egbert Rijke
2022-12-23 14:22 ` João Alves Silva Júnior
2022-12-23 22:51 ` 'EMILY RIEHL' via Homotopy Type Theory
2023-01-03 19:16 ` 'Urs Schreiber' via Homotopy Type Theory
2023-01-03 22:05   ` Jon Sterling
2023-01-13 14:52     ` Madeleine Birchfield

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).