From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 29047 invoked from network); 13 Jan 2023 14:55:46 -0000 Received: from mail-yb1-xb38.google.com (2607:f8b0:4864:20::b38) by inbox.vuxu.org with ESMTPUTF8; 13 Jan 2023 14:55:46 -0000 Received: by mail-yb1-xb38.google.com with SMTP id l194-20020a2525cb000000b007b411fbdc13sf23255111ybl.23 for ; Fri, 13 Jan 2023 06:55:46 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:sender:from :to:cc:subject:date:message-id:reply-to; bh=LqcO1L61gsnRw7E5BocFzZz5ivvS47wjWiD8Yfg2dS8=; b=SW7kiYzmtMUp25UEX7CJGq+o32n/LLFjfmbrsd6Q3r4equi+b6TVtWDewAwBbB3vhM QnUG+8VQhKyaSAqHY0bbpiP8vnqwJE1Dwai+mpfCaUj28TKjeIF3gYyRfrj8zCTAl0Hw J4jj1jnYTA9lD1I5te1FaHbwYf+v5x8d4xdTVc4LzIL/em1nclZROL00uHDLv634rnOS UcjqS18LvMC3YzNkSVfqLhixwEViWEsiIRvklUk2FjXKGkhoX+aTWA51yW5HoFes8j2l WIwCKFZxP8uC/njOUVQO0FODaEtl8u+uGbDfood1Pffk85K3QUk4rb1OjJWFFxCps4Fj ucRw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:from:to:cc :subject:date:message-id:reply-to; bh=LqcO1L61gsnRw7E5BocFzZz5ivvS47wjWiD8Yfg2dS8=; b=hj3tw4cd05IdeRPBrEC/i+DH2EBErBZvoIkidH9uyyYWv/rlXOp+4wjA3DDHfUEAZA b5+eoAGej5iUBnJnM5SCC4w7/uO16xZux/WhrAusHzayKg1WAqaQqP/34+TOre1IYDKv bbCwHU/iMw2VEbi3eBZjZxL+98l+dPHc3B4AUNS0K126O+cJNpiBZcm5gEzo1r4rXiml JJ08RJhhxVpcbqur1tNBHGbl6BkkuPz5FwZhu6qXCdb+FtpTdJFICKZkcdw6a+GrNMjt BeFRXXmwJZrG9XKga2BbTZfRWlPvGnbtKCbTvE1qc9E8dm7CeBE+d6oq3Qf2K0mIjDIh RUYQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=LqcO1L61gsnRw7E5BocFzZz5ivvS47wjWiD8Yfg2dS8=; b=kBEWNIIW4+OWCTOjblWvFal9IF8UrfsudZLM12rg7AS9VDYZzl5IF6sWlhtq8MY0hh qA+ecWaLo2Htphp3pv9aeFthJh3A7MN+uSde/Ryu70+dLqrv30ZkkExAUUdaZP+Lz70W TKZQZKInAH7QNTxkkQJ5jpZxvuTv7x6iJ+9/qTgBMAh0uJ1Amqoka4jKetSzYif7f+cJ 9BmTmV3FHkidP72yeFXf7K/JRVDDOaHoT51EKkBbuhBeQd0eLo24iSRvxPqo77BoaUYu 1mFBQxwdYHm2Cq0bNnDJ/enH1OR5jDvkuzinIlJQ6/AiwQczTbgm5vbLrjuvGq4o4FD0 OaYw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AFqh2koU68uYvFy3ojw6zNBYfcIGSPdMCwUmwk9WC7iyTbPMPnGDlktT kCoqXBx1pkxlg1y/fOcQ9UA= X-Google-Smtp-Source: AMrXdXsacSJBJmuKLTe8sSfiEaOY4ylFZolgdO/meNrrYYSO9klFDaPfAx1RxviyMosOtqT76Wlq5Q== X-Received: by 2002:a81:ecb:0:b0:4de:4a0f:8658 with SMTP id 194-20020a810ecb000000b004de4a0f8658mr329216ywo.0.1673621744217; Fri, 13 Jan 2023 06:55:44 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:8083:0:b0:3da:3e43:9e3c with SMTP id q125-20020a818083000000b003da3e439e3cls2922474ywf.9.-pod-prod-gmail; Fri, 13 Jan 2023 06:55:43 -0800 (PST) X-Received: by 2002:a0d:d811:0:b0:475:d2f4:6522 with SMTP id a17-20020a0dd811000000b00475d2f46522mr2526707ywe.120.1673621743221; Fri, 13 Jan 2023 06:55:43 -0800 (PST) Received: by 2002:a81:5558:0:b0:46f:5fd1:6cdb with SMTP id 00721157ae682-4de538d9e73ms7b3; Fri, 13 Jan 2023 06:52:23 -0800 (PST) X-Received: by 2002:a81:6d85:0:b0:3f2:e8b7:a6ec with SMTP id i127-20020a816d85000000b003f2e8b7a6ecmr2862674ywc.332.1673621543039; Fri, 13 Jan 2023 06:52:23 -0800 (PST) Date: Fri, 13 Jan 2023 06:52:22 -0800 (PST) From: Madeleine Birchfield To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_5060_1958741652.1673621542765" X-Original-Sender: madeleinebirchfield@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , ------=_Part_5060_1958741652.1673621542765 Content-Type: multipart/alternative; boundary="----=_Part_5061_544364600.1673621542765" ------=_Part_5061_544364600.1673621542765 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Congratulations on finishing this textbook, Egbert! This textbook, in its= =20 draft format, has been very useful in my learning of homotopy type theory= =20 as a foundations of mathematics back a few years ago, and I'm glad to see= =20 it finished and hopefully published and available in hardcover format soon.= =20 As for the splitting of the textbook in two, I actually agree with the=20 decision to remove the material on using homotopy type theory for synthetic= =20 homotopy theory from the textbook, so that this textbook focuses on the=20 foundational aspects of homotopy type theory. However, I do have to agree= =20 with Jon that I hope the second half of the textbook gets published as its= =20 own textbook; my preferred title would probably be "Synthetic Homotopy=20 Theory" since much of the removed material was specifically about synthetic= =20 homotopy theory.=20 Thanks, Madeleine Birchfield On Tuesday, January 3, 2023 at 11:06:11 PM UTC+1 j...@jonmsterling.com=20 wrote: > Hi all, > > I second Urs's congratulations on this great achievement! Just want to=20 > also add that I likewise miss the material on descent & flattening, for= =20 > which your old notes provided an excellent reference. Of course, perhaps= =20 > this leaves room for an "Advanced Topics in Homotopy Type Theory" followu= p=20 > ;-) > > 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 wrote: > >> > >> Dear homotopy type theorists, > >> > >> My textbook Introduction to Homotopy Type Theory is finished and=20 > available on the ArXiv: > >> > >> https://arxiv.org/abs/2212.11082 > >> > >> From the abstract: > >> This is an introductory textbook to univalent mathematics and homotopy= =20 > type theory, a mathematical foundation that takes advantage of the=20 > structural nature of mathematical definitions and constructions. It is=20 > common in mathematical practice to consider equivalent objects to be the= =20 > same, for example, to identify isomorphic groups. In set theory it is not= =20 > possible to make this common practice formal. For example, there are as= =20 > many distinct trivial groups in set theory as there are distinct singleto= n=20 > sets. Type theory, on the other hand, takes a more structural approach to= =20 > the foundations of mathematics that accommodates the univalence axiom.=20 > This, however, requires us to rethink what it means for two objects to be= =20 > equal. This textbook introduces the reader to Martin-L=C3=B6f's dependent= type=20 > theory, to the central concepts of univalent mathematics, and shows the= =20 > reader how to do mathematics from a univalent point of view. Over 200=20 > exercises are included to train the reader in type theoretic reasoning. T= he=20 > book is entirely self-contained, and in particular no prior familiarity= =20 > with type theory or homotopy theory is assumed. > >> > >> Over Christmas I will write a blog post in which I will go more into= =20 > the content of the book. For now: Enjoy! > >> > >> Happy holidays to everyone! > >> Egbert > >> > >> -- > >> You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > >> To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeThe...@googlegroups.com. > >> To view this discussion on the web visit=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEek= jwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com > . > > > > --=20 > > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeThe...@googlegroups.com. > > To view this discussion on the web visit=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BKbugeyU16TCLH9M= biBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODHA%40mail.gmail.com > . > --=20 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 e= mail 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= . ------=_Part_5061_544364600.1673621542765 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Congratulations on finishing this textbook, Egbert! This textbook, in its d= raft 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 wit= h the decision to remove the material on using homotopy type theory for syn= thetic homotopy theory from the textbook, so that this textbook focuses on = the foundational aspects of homotopy type theory. However, I do have to agr= ee with Jon that I hope the second half of the textbook gets published as i= ts own textbook; my preferred title would probably be "Synthetic Homotopy T= heory" since much of the removed material was specifically about synthetic = homotopy theory.

Thanks,

Madeleine Birchfi= eld

On Tuesday, January 3, 2023 at 11:06:11 PM UTC+1 j...@jonmsterl= ing.com wrote:
https://www.andrew.cmu.edu/user/erijke/hott/hott= _intro.pdf), which
> have discussion for instance of homotopy pullbacks/pushouts that s= eem
> 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 d= ecision,
> but just to say that if there is any wiggle room left, then I woul= d
> think it most worthwhile if these topics could make it into the fi= nal
> 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 a= nd 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 com= mon in mathematical practice to consider equivalent objects to be the same,= for example, to identify isomorphic groups. In set theory it is not possib= le to make this common practice formal. For example, there are as many dist= inct trivial groups in set theory as there are distinct singleton sets. Typ= e theory, on the other hand, takes a more structural approach to the founda= tions of mathematics that accommodates the univalence axiom. This, however,= requires us to rethink what it means for two objects to be equal. This tex= tbook introduces the reader to Martin-L=C3=B6f'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 i= ncluded to train the reader in type theoretic reasoning. The book is entire= ly 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 mor= e into the content of the book. For now: Enjoy!
>>
>> Happy holidays to everyone!
>> Egbert
>>
>> --
>> You received this message because you are subscribed to the Go= ogle Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from = it, send an email to HomotopyTyp= eThe...@googlegroups.com.
>> To view this discussion on the web visit https://group= s.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B= 1te2ZLX%2BNZsQLeChxg%40mail.gmail.com.
>
> --=20
> 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.c= om/d/msgid/HomotopyTypeTheory/f641a5c8-ea0b-4e82-a2f2-c9c1a8205d94n%40googl= egroups.com.
------=_Part_5061_544364600.1673621542765-- ------=_Part_5060_1958741652.1673621542765--