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 16594 invoked from network); 23 Dec 2022 09:54:40 -0000 Received: from mail-ej1-x63b.google.com (2a00:1450:4864:20::63b) by inbox.vuxu.org with ESMTPUTF8; 23 Dec 2022 09:54:40 -0000 Received: by mail-ej1-x63b.google.com with SMTP id sg39-20020a170907a42700b007c19b10a747sf3160225ejc.11 for ; Fri, 23 Dec 2022 01:54:40 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1671789279; cv=pass; d=google.com; s=arc-20160816; b=080mp30aah+i7FvilSz5pd8JVfTDjVWALj7lhJVPOYQ2yW5HoCWSOfzFUwqPdPmZyb Nfr+cyLQv2xh6Jj4jLKpYkQntgEKdASRF3VlqSxXY2UFUzYQWV5VrBR+4ot6zmODXqC6 mcAdUmaQTOXW7+rfJ31xdP8yHa/Nc04voRroXl9U8JH8EVGWVGIf5Q6F3S4StR743mQ5 JOoJhzB+hyTx34p7Tq4JwEV3oL/XaCMxEmp+a1+BtUG8A/DAYi6Rmc7blLKlCkxMDBDD mvZG+SXVi7wrWK7lPGTXaoDPHlPS/AZAehlDaT7aNH3WQls0rbQm+7E2KjDrHqyUv7KP +8OA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=ZmDkKoMt+ONvU8cR8W83DpQ40eEeQP290ZREZ4fay9M=; b=mKnMaw8ZbRWBvx1cgN5LTkAdzGEuunOZAdnyYzSsbKPw8e6UDL3gza+mY08onIjRls G/KALEV188KaOSdCreFlUVVOVF/g3AFycWi9fN1fGKO5OcAGAhqKLfpqUGFzK7mW7oY6 0K5UVkwuo/JEBc2SmXPshX8iA6fzPLRoBnpA1yKu2gGCulevON5NGangIOZqxGejP+Ci hUyCtagUomBVNTxcz+ZZuKmDUkU9G4tgUgOnyCAsMjM1AF2jouXyIFerr3odpZEUDb22 cGTxwFS7N+scRCSRrryZ6AikSrPyAZq8fHiYza4dkAY+fbXu2dP5sIQwFuYILb/c11ev ZOKw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=IQr0b8dE; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::62d as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version :sender:from:to:cc:subject:date:message-id:reply-to; bh=ZmDkKoMt+ONvU8cR8W83DpQ40eEeQP290ZREZ4fay9M=; b=UwT3CydsRQRF1s3WD9VhLVvL1rt0dwbTsV/6vZgm33X5WqDQwXt/om7fgKZgaKAHU5 GOYuh9hbv/zVWtRuemDiw/OJ9culBN3DzLh2HPOMYhRXiEErZ/LWu9y4sgIVh5y8JEQL UuEkzG0DBZVdRzAI3vVg+POXi05tdjN26n3CDnQ1//FLL02r57LZqpDAeNrska1HdsT0 lmiy5bJD4c4som0W1MZL7Ot21UqTXrSKIRSEAwNmmHRvOIxTQd6Qkkv+aRSc0nxESNJE HLxS2Eac1Lrn+R3t9Fu6QT5w3HEYRTdWMD08ymfRlLNahgWmHOpo71ycrzFWUi+WQWiP 8ASA== 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-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version:from :to:cc:subject:date:message-id:reply-to; bh=ZmDkKoMt+ONvU8cR8W83DpQ40eEeQP290ZREZ4fay9M=; b=Nw9MVekV96j6Yj4m0AUTf4bKTjTKSbOh8Vs33agdzrl3EoY6W4okvYjKGQmaIpYvnp uzZWWVYTz+pbY0FxR+diliFtw7kNS3M2CojiSdkXiKz3VsWgbXfMi2uU9BJNcc4QcTwx 9IAKSveldSODpjHdDVIi7pSqsqFuQmG4ttt/egk2XrdOdAeVD+OFJniz3xOo5/8I2wQZ g0rza/n9ZV3aGcH0Nxc3iezQogwbOWnrPoQHA2i3dHwTAwEG9QZRtnjmy6956vocsVH+ MrPCGOLTmw2UjuvSKmCSBkXDC36uUs4AFxv56s4Fg51EZ3m1w4ihSlOsh0r6cOnRI5Bj 7/qQ== 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 :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:to:subject :message-id:date:from:mime-version:x-gm-message-state:sender:from:to :cc:subject:date:message-id:reply-to; bh=ZmDkKoMt+ONvU8cR8W83DpQ40eEeQP290ZREZ4fay9M=; b=ZTL+KnfeqV/C+XrNeZjemlgpaL/iSpBhi8irVMjUC2q8zADukRVFLZ6P3sLc4TTCew asivC3E4VAsHDkl2s5D+wRz9K6Y1XH0Ec0df5nv8k/VoINA679add1ADXz0oilg6STkp ck0Spj7/4z7l6FJeUPC//iNcP2Hh/Fb89iocQ38lbx03uLYlxP5Y76q94wqJJPLZesWB klMZkO87RvSmTOfWxu6IqGeF5gb2+mRAXK1M/cV/2ucPKF+t5mlKPVlupkx6+RiGXv26 J3VcIW2I4JX/h7ZxaInw+rMYvic/xD1CGLfYJEphEBbrcdhGNehb5rvcE88cuVUferUW XmvA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AFqh2ko9zGrSNs4WiFjefCd02Y9fHJhWgDrZZK5bgTAZ9XMa2GmKAYou oAdssaU0fOQpKkUIisIRO6Y= X-Google-Smtp-Source: AMrXdXvAiG3DEth2Ym0ra979AInJS2HfauQe6QsXUF+kI61GXO9KpyrWbQYqDtyufMifutjX7K7hbw== X-Received: by 2002:a17:906:d90:b0:7c1:a0e:77 with SMTP id m16-20020a1709060d9000b007c10a0e0077mr913692eji.29.1671789279295; Fri, 23 Dec 2022 01:54:39 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:2302:b0:7c0:b9d9:60f3 with SMTP id l2-20020a170906230200b007c0b9d960f3ls2637787eja.9.-pod-prod-gmail; Fri, 23 Dec 2022 01:54:36 -0800 (PST) X-Received: by 2002:a17:907:d68e:b0:7bd:43e9:d3ab with SMTP id wf14-20020a170907d68e00b007bd43e9d3abmr6854517ejc.52.1671789276876; Fri, 23 Dec 2022 01:54:36 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1671789276; cv=none; d=google.com; s=arc-20160816; b=KzJD5P0kpznT9Lvn/f9uTlm/F8Ze/onJqLnppiruUngnIEJ/xIJ94hcWrbcTxf8Ss6 B1NSls3qQMwV8SNbUm9PfuSbK8sysfDKdvTAsiPUNT8NOK/KYLDADbwdLoSHNOEnWHB1 SuEI/7WDGVEA9tlIqk6SQrST2kB5q89mbo5r8p0GJ+jFFozT1ATdQ19Qrf/w2LkK2hiJ L74uLp3y2EbAn2aOfKMdKr8Tp2Q7hB5HYXwt0wQGch3rcsp5rdHicXXRXVD9F90o5eJb D3ZnCAniw9zs9RnErY5zW6S0qklXLnYpj8GYHzHRWAlxhRo92d8u5xfCx41HXSTToSOJ LRvg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=yfxWavlMuWNQ28NThh8uCT96Lx1b3b+P1Qf+mOXNePw=; b=FfHykDAdAOFpCBhZJO12wkT3t4WOjujfXNXCqCdkFAu/3CdVeGCIui+8xAguyhyWwo rskJnoCqUFQdV43eBuADirwJH+IA1gxqom2AAU/lvzXfdR1NJwkTxlI/kQcAG4s7kWg+ pYLBm/p4csjzD3ST/2EUGBrfcGfOsTNmhH6XZpPgD+wEBudTZxCzQndBrUut5CWq+8bQ kbh9ENFyDem4XyITYEGd5s5i7FuViZNhDmWuuE3dBYcNv51bwjRHQ4dHuLSNpSWwDUmN QKIhJBjN634eZG0SP+VzsiVwgzEb4pb1UEqtv/yCgn8wDieV65iPTLwE4wF9Lz5Bu83F AmoQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=IQr0b8dE; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::62d as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ej1-x62d.google.com (mail-ej1-x62d.google.com. [2a00:1450:4864:20::62d]) by gmr-mx.google.com with ESMTPS id mm6-20020a170906cc4600b007c16d82962dsi129750ejb.0.2022.12.23.01.54.36 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 23 Dec 2022 01:54:36 -0800 (PST) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::62d as permitted sender) client-ip=2a00:1450:4864:20::62d; Received: by mail-ej1-x62d.google.com with SMTP id t17so10966370eju.1 for ; Fri, 23 Dec 2022 01:54:36 -0800 (PST) X-Received: by 2002:a17:906:7d0:b0:7c1:19e1:50e6 with SMTP id m16-20020a17090607d000b007c119e150e6mr895655ejc.585.1671789276074; Fri, 23 Dec 2022 01:54:36 -0800 (PST) MIME-Version: 1.0 From: Egbert Rijke Date: Fri, 23 Dec 2022 10:54:24 +0100 Message-ID: Subject: [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000f0959e05f07bc513" X-Original-Sender: E.M.Rijke@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=IQr0b8dE; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::62d as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --000000000000f0959e05f07bc513 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=C3=B6f's dependent type the= ory, 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 --=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/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%= 40mail.gmail.com. --000000000000f0959e05f07bc513 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear homotopy type theorists,

My textbook Introduct= ion to Homotopy Type Theory is finished and available on the ArXiv:

= https://arxiv.org/abs/2212.110= 82

From the abstract:
This is an introductory textbook to uni= valent mathematics and homotopy type theory, a mathematical foundation that= takes advantage of the structural nature of mathematical definitions and c= onstructions. 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 disti= nct singleton sets. Type theory, on the other hand, takes a more structural= approach to the foundations of mathematics that accommodates the univalenc= e axiom. This, however, requires us to rethink what it means for two object= s to be equal. This textbook introduces the reader to Martin-L=C3=B6f's= dependent type theory, to the central concepts of univalent mathematics, a= nd shows the reader how to do mathematics from a univalent point of view. O= ver 200 exercises are included to train the reader in type theoretic reason= ing. The book is entirely self-contained, and in particular no prior famili= arity with type theory or homotopy theory is assumed.

Ov= er Christmas I will write a blog post in which I will go more into the cont= ent of the book. For now: Enjoy!

Happy holidays to= everyone!
Egbert

--
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.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%= 2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com.
--000000000000f0959e05f07bc513--