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

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

[Egbert Rijke]

[-- 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 --]

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

[João Alves Silva Júnior]

[-- 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 --]

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

['EMILY RIEHL' via Homotopy Type Theory]

Congratulations Egbert!

Last fall I taught a topics course on homotopy type theory following this book to an audience of mostly mathematics students. The weekly problem sets were all in Agda, drawing inspiration from Egbert's excellent lists of exercises and extensive formalized library. Course materials are available here: https://github.com/emilyriehl/721

I mention all of this to say that I had an excellent experience teaching using Egbert's book. I had to skip several topics due to time constraints but I never found myself wishing the material were presented in a different order, which is quite remarkable. Kudos Egbert!

Emily

Professor of Mathematics (she/her)
Johns Hopkins University
emilyriehl.github.io

On 12/23/22 04:54, Egbert Rijke wrote:
> Dear homotopy type theorists,
> 
> My textbook Introduction to Homotopy Type Theory is finished and available on the ArXiv:
> 
> https://arxiv.org/abs/2212.11082 <https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Farxiv.org%2Fabs%2F2212.11082&data=05%7C01%7Ceriehl%40jhu.edu%7C0aa33ca5d7df4698161908dae4cbb6a2%7C9fa4f438b1e6473b803f86f8aedf0dec%7C0%7C0%7C638073860853350577%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=aVyJRuhCTZwnztt1H3l2aQMOvn2sfNUVD%2B0obnR%2FC0Y%3D&reserved=0>
> 
> 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 <mailto: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://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2FHomotopyTypeTheory%2FCAGqv1ODuH3xtsFyFEekjwNH4SUN%252BdU8B1te2ZLX%252BNZsQLeChxg%2540mail.gmail.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=05%7C01%7Ceriehl%40jhu.edu%7C0aa33ca5d7df4698161908dae4cbb6a2%7C9fa4f438b1e6473b803f86f8aedf0dec%7C0%7C0%7C638073860853350577%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=yP5HBchPgpQNsZlwcNVENWmOKZeHdVBHkSneMgvzjCc%3D&reserved=0>.

-- 
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/7e2fee3c-30e8-a3ec-8941-68c63538240b%40jh.edu.

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

['Urs Schreiber' via Homotopy Type Theory]

Hi Egbert,

nice to see your notes now available in a stably referenceable way!
They could fill quite a few gaps that the existing textbook literature
leaves open.

On that note, it seems that a fair bit of material has been removed in
the arXiv version?
(Maybe to make room for large margins?)

For referencing on the nLab I now find myself pointing mainly to the
version of your notes from 2018 (these here:
https://www.andrew.cmu.edu/user/erijke/hott/hott_intro.pdf), which
have discussion for instance of homotopy pullbacks/pushouts that seem
to have later been dropped, together with much material depending on
these notions (if I am seeing this correctly ?)

I can imagine this is at least in large part the publisher's decision,
but just to say that if there is any wiggle room left, then I would
think it most worthwhile if these topics could make it into the final
book version.

All my best wishes for the New Year,
Urs

On Fri, Dec 23, 2022 at 1:54 PM Egbert Rijke <e.m.rijke@gmail.com> wrote:
>
> 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.

-- 
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/CA%2BKbugeyU16TCLH9MbiBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODHA%40mail.gmail.com.

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

[Jon Sterling]

Hi all,

I second Urs's congratulations on this great achievement! Just want to also add that I likewise miss the material on descent & flattening, for which your old notes provided an excellent reference. Of course, perhaps this leaves room for an "Advanced Topics in Homotopy Type Theory" followup ;-)

Best,
Jon


On 3 Jan 2023, at 20:16, 'Urs Schreiber' via Homotopy Type Theory wrote:

> Hi Egbert,
>
> nice to see your notes now available in a stably referenceable way!
> They could fill quite a few gaps that the existing textbook literature
> leaves open.
>
> On that note, it seems that a fair bit of material has been removed in
> the arXiv version?
> (Maybe to make room for large margins?)
>
> For referencing on the nLab I now find myself pointing mainly to the
> version of your notes from 2018 (these here:
> https://www.andrew.cmu.edu/user/erijke/hott/hott_intro.pdf), which
> have discussion for instance of homotopy pullbacks/pushouts that seem
> to have later been dropped, together with much material depending on
> these notions (if I am seeing this correctly ?)
>
> I can imagine this is at least in large part the publisher's decision,
> but just to say that if there is any wiggle room left, then I would
> think it most worthwhile if these topics could make it into the final
> book version.
>
> All my best wishes for the New Year,
> Urs
>
> On Fri, Dec 23, 2022 at 1:54 PM Egbert Rijke <e.m.rijke@gmail.com> wrote:
>>
>> 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.
>
> -- 
> 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/CA%2BKbugeyU16TCLH9MbiBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODHA%40mail.gmail.com.

-- 
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/B7706C57-2DE8-4AB6-A50B-89F7E6C1067D%40jonmsterling.com.

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

[Madeleine Birchfield]

[-- Attachment #1.1: Type: text/plain, Size: 5417 bytes --]

Congratulations on finishing this textbook, Egbert! This textbook, in its 
draft format, has been very useful in my learning of homotopy type theory 
as a foundations of mathematics back a few years ago, and I'm glad to see 
it finished and hopefully published and available in hardcover format soon. 

As for the splitting of the textbook in two, I actually agree with the 
decision to remove the material on using homotopy type theory for synthetic 
homotopy theory from the textbook, so that this textbook focuses on the 
foundational aspects of homotopy type theory. However, I do have to agree 
with Jon that I hope the second half of the textbook gets published as its 
own textbook; my preferred title would probably be "Synthetic Homotopy 
Theory" since much of the removed material was specifically about synthetic 
homotopy theory. 

Thanks,

Madeleine Birchfield

On Tuesday, January 3, 2023 at 11:06:11 PM UTC+1 j...@jonmsterling.com 
wrote:

> Hi all,
>
> I second Urs's congratulations on this great achievement! Just want to 
> also add that I likewise miss the material on descent & flattening, for 
> which your old notes provided an excellent reference. Of course, perhaps 
> this leaves room for an "Advanced Topics in Homotopy Type Theory" followup 
> ;-)
>
> Best,
> Jon
>
>
> On 3 Jan 2023, at 20:16, 'Urs Schreiber' via Homotopy Type Theory wrote:
>
> > Hi Egbert,
> >
> > nice to see your notes now available in a stably referenceable way!
> > They could fill quite a few gaps that the existing textbook literature
> > leaves open.
> >
> > On that note, it seems that a fair bit of material has been removed in
> > the arXiv version?
> > (Maybe to make room for large margins?)
> >
> > For referencing on the nLab I now find myself pointing mainly to the
> > version of your notes from 2018 (these here:
> > https://www.andrew.cmu.edu/user/erijke/hott/hott_intro.pdf), which
> > have discussion for instance of homotopy pullbacks/pushouts that seem
> > to have later been dropped, together with much material depending on
> > these notions (if I am seeing this correctly ?)
> >
> > I can imagine this is at least in large part the publisher's decision,
> > but just to say that if there is any wiggle room left, then I would
> > think it most worthwhile if these topics could make it into the final
> > book version.
> >
> > All my best wishes for the New Year,
> > Urs
> >
> > On Fri, Dec 23, 2022 at 1:54 PM Egbert Rijke <e.m....@gmail.com> wrote:
> >>
> >> 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 HomotopyTypeThe...@googlegroups.com.
> >> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com
> .
> >
> > -- 
> > 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 HomotopyTypeThe...@googlegroups.com.
> > To view this discussion on the web visit 
> https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BKbugeyU16TCLH9MbiBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODHA%40mail.gmail.com
> .
>

-- 
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/f641a5c8-ea0b-4e82-a2f2-c9c1a8205d94n%40googlegroups.com.

[-- Attachment #1.2: Type: text/html, Size: 7779 bytes --]