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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 11867 invoked from network); 3 Jan 2023 19:16:41 -0000 Received: from mail-ed1-x53d.google.com (2a00:1450:4864:20::53d) by inbox.vuxu.org with ESMTPUTF8; 3 Jan 2023 19:16:41 -0000 Received: by mail-ed1-x53d.google.com with SMTP id w18-20020a05640234d200b0048cc3aa4993sf4675568edc.7 for ; Tue, 03 Jan 2023 11:16:41 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1672773400; cv=pass; d=google.com; s=arc-20160816; b=CXFM3R8ckMHS9EvcVOzDG1tZD6mbCdGDkX5aQzQmfYZmjv/wJr/6nAJz2hldi9tNqV oqlbuKS7YfgPiPbHEPb/7d6/eTjd8HP7INVT2/5ohu7w5qlhcmvCdePJ0IMAAVN+363j riomd0sMJMk7jAttC963wXQWoLC+TxvFsHMSNF9KhNIxgXUV4N+lGWlem8ST4PGa/wlq hpwXlCGu7RAp0FDnAnq/K8JstIKyVDJn9o4XLOwmwJECblTw1eQj9+xrpboKku4pE8qE Ijzl0yyiryAeTEWdjQKdouwts03T4D0TE28tWW+1FDZKzqG4XiQXk789K6bHwGifqrRH AVlQ== 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:reply-to:content-transfer-encoding :cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=oRA4wNFion4VY37XWcg/jxEGmsESxGNKcSosCWPbed4=; b=higGt+LjgkzL0+OPYVDvttcFz7bFl4Iz/WTr2gd0ESbGlhKsjfaUYrazPqS9CTMo6y ebuMUXDejM2TLdgxLQTP+Lj4X+DE1TpAYMEJuEHhNJpm6Y7yTnOTpuJIyytWPmNPZyvB XhMX7ME70GaaCvOdykf1lpUNTugYHL08XyazQvWjA1kPXri2KE6/hrTBeDbHVb6QhLt8 eEgpuH3Z/SLEeYcn5nYAYFXHMpoPlGrlvsVNn2xx9O2CS7/CNTltLUG8kIkPupT55RLF 4ROD2MXhYgdJFVnUFJQBi3wVwJurmoLqcB+DFnsFzCtkeHe/zP0jTJYti6v+CyEGJGyG 0MAQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20210112 header.b=eVNzLPwc; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2a00:1450:4864:20::32c as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.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:reply-to :x-original-authentication-results:x-original-sender :content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:from:to:cc:subject:date :message-id:reply-to; bh=oRA4wNFion4VY37XWcg/jxEGmsESxGNKcSosCWPbed4=; b=XMm1N9ye2DkgpxyfpnDKqK698V0YwR4TcIBJo8kHNaeDzfx303hfz1aT28LOT/pzy7 wf8oSGqHzISY6BydYtVx7KS2iRhGoWpoQ9msMjmvhL+bGrEWIqR0Rxu1bvoPGmEQh2Rx G96LcDs/fUQ8vjTXIccZKabonpEBU14EhM5YnNRsfLvd3Sj/Sr5ADUfgKkdAHmH9dZEC tnHaKQ1+omubOMsr224z0a9GGf3naad78zcZXCQltS0tGG21ZfYG60BkTcSWQieKHGi/ fohnlnCP9mPqdFk5Cawb0gVKj2b/8ClbE9UqBP+Wek+GNVuxxZ7JmHifjoW4sntUpaHe B2zQ== 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:reply-to :x-original-authentication-results:x-original-sender :content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=oRA4wNFion4VY37XWcg/jxEGmsESxGNKcSosCWPbed4=; b=ibCPApPLTBRhIeqQbr8PX4DziLo/Oovqc+zbjMFnT5G3ayRNv38iBaRl3V4G4IqgKq /DIgKmxlJ3+OwhBtScvMDfALCSg55A5/bPI2MM3QsHsWB0XW5UhLiywF5igMOpa/lpzk uTVjboX4WSBt6fq8c7X/RVjJfknTcgf7t/GNIBps5L/IgTOBSMGk66Df9RycXrgaKgWA lgrVXvOfmkMEYL0Gv98nFJUaiGzKy/HjoGw+WwCrwFYgJNjieBnZCE6rryp+ll2XxLXc 2T0oi3MIooMzRMAxvKU37wAvkvAwgjD1yMeZfWl4y9voM8BuywwcvJmBQ+sMstf3gPqA M14g== X-Gm-Message-State: AFqh2kokV7eETGKFQU+FO+WmCYegWbcQjONxHMLl69utlJ0ZrNK6piZX uXv6kXyOJJJ1oO43lX69rHc= X-Google-Smtp-Source: AMrXdXtzL/7RTR7lUHGLIkea/ZkerZmnr+E7/aIzLiyYM4ik/T43nIonRRpEkzV+6LQnf5+l0XlRig== X-Received: by 2002:a17:906:3a85:b0:7c0:b56a:eadf with SMTP id y5-20020a1709063a8500b007c0b56aeadfmr4781177ejd.271.1672773400260; Tue, 03 Jan 2023 11:16:40 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6402:40d5:b0:479:6c1:ef04 with SMTP id z21-20020a05640240d500b0047906c1ef04ls3814525edb.0.-pod-prod-gmail; Tue, 03 Jan 2023 11:16:37 -0800 (PST) X-Received: by 2002:aa7:c1d5:0:b0:489:64aa:d1aa with SMTP id d21-20020aa7c1d5000000b0048964aad1aamr21077804edp.16.1672773397672; Tue, 03 Jan 2023 11:16:37 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1672773397; cv=none; d=google.com; s=arc-20160816; b=X27EgTFxcXedRutSoLEtckKAShH6j2RcE0fqevsR5EVoSndFIYEFbpJViajBdBl0dK RP+81op2i+KwvKCJqjjcIjSfIw57K5AdfB43N1inNbjGE7tVvzhOO2HKThtKza7Y59z3 KqzPPtzYMzTTLp9hR0ACL4LuUkxuC9hpbzu9IgoZoLApLhaWvh7VBtNMa7gPL8NdMlHX wxmEfw/PWEddBKxCtXnnYSaVShh0Wl2Wkf6c2PyQxM5QRaKblV5kvifn102WLW0XGa+e XQjVWAMYLuQNpK0c0JHJvQNlBJpg+7d5LmvZForWje06ZMdXvPm2nXJhrw51ZFTJErUc BqGQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=Aso5vUKSJ7LRwvPfSGgEt2y2ThJfpZ0qnxMShkjGaso=; b=cRjtFQjC8F95QWyDqFSsPlKRFitZlwwC9QBrcTm/OK1Hy/wgNk+PRDyPkA6VntUfK4 TFvyOfOdLPENadStKXVBPC2Fep+k8/d1TJ9OW0CJFak2Fxo68OEYu/Osid0HZsV75ODd PtJ4uhDYbh99XuLPr31v12k8Jyo7YpQ8Lbgk0B0iA+SLHEmBDDd/CdRpHkpdqppxAqNj ueFtgb+SUhprgfrzZXBOefPL1URuYZDz57NDmXrxlx4Q8GVQXyxczjb4AAjrRnE8Fodr lUUeOt+vdSXLBBMX4tAQ4+OY5ibN7Ap+bYGAj7mxjEogTqFxqt1sL3EFbnWTmghCL4Yl hhuA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20210112 header.b=eVNzLPwc; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2a00:1450:4864:20::32c as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com Received: from mail-wm1-x32c.google.com (mail-wm1-x32c.google.com. [2a00:1450:4864:20::32c]) by gmr-mx.google.com with ESMTPS id r8-20020aa7d148000000b0048ecd372fccsi100694edo.5.2023.01.03.11.16.37 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 03 Jan 2023 11:16:37 -0800 (PST) Received-SPF: pass (google.com: domain of urs.schreiber@googlemail.com designates 2a00:1450:4864:20::32c as permitted sender) client-ip=2a00:1450:4864:20::32c; Received: by mail-wm1-x32c.google.com with SMTP id bg13-20020a05600c3c8d00b003d9712b29d2so21691094wmb.2 for ; Tue, 03 Jan 2023 11:16:37 -0800 (PST) X-Received: by 2002:a7b:c457:0:b0:3a5:cb0e:8242 with SMTP id l23-20020a7bc457000000b003a5cb0e8242mr2868733wmi.188.1672773397266; Tue, 03 Jan 2023 11:16:37 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: "'Urs Schreiber' via Homotopy Type Theory" Date: Tue, 3 Jan 2023 23:16:50 +0400 Message-ID: Subject: Re: [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv To: Egbert Rijke Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: urs.schreiber@googlemail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20210112 header.b=eVNzLPwc; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2a00:1450:4864:20::32c as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com X-Original-From: Urs Schreiber Reply-To: Urs Schreiber 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: , 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 availabl= e on the ArXiv: > > https://arxiv.org/abs/2212.11082 > > From the abstract: > This is an introductory textbook to univalent mathematics and homotopy ty= pe theory, a mathematical foundation that takes advantage of the structural= nature of mathematical definitions and constructions. It is common in math= ematical practice to consider equivalent objects to be the same, for exampl= e, to identify isomorphic groups. In set theory it is not possible to make = this common practice formal. For example, there are as many distinct trivia= l groups in set theory as there are distinct singleton sets. Type theory, o= n the other hand, takes a more structural approach to the foundations of ma= thematics that accommodates the univalence axiom. This, however, requires u= s to rethink what it means for two objects to be equal. This textbook intro= duces 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 mathemat= ics from a univalent point of view. Over 200 exercises are included to trai= n the reader in type theoretic reasoning. The book is entirely self-contain= ed, and in particular no prior familiarity with type theory or homotopy the= ory 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/msgi= d/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChx= g%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/CA%2BKbugeyU16TCLH9MbiBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODHA%= 40mail.gmail.com.