Re: [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv

["João Alves Silva Júnior" <jasj@dmat.ufpe.br>]

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

Thank you!

Em sex., 23 de dez. de 2022 06:54, Egbert Rijke <e.m.rijke@gmail.com>
escreveu:

> 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
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>

-- 
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/CABUO1-ihPx2Zugxh9YbWA626Dc4uyQuaCtrxvHTGuLog%2Bza49g%40mail.gmail.com.

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