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.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 32739 invoked from network); 3 Jan 2023 22:06:13 -0000 Received: from mail-yb1-xb3a.google.com (2607:f8b0:4864:20::b3a) by inbox.vuxu.org with ESMTPUTF8; 3 Jan 2023 22:06:13 -0000 Received: by mail-yb1-xb3a.google.com with SMTP id t13-20020a056902018d00b0074747131938sf31805951ybh.12 for ; Tue, 03 Jan 2023 14:06:13 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1672783571; cv=pass; d=google.com; s=arc-20160816; b=O+dSAJ2UlIzSvuk4vGIy8DRtOppm2INLmbWVNmgRVQC+fgzMPDCK/pBtiWtqblJg6l Q0cjY+UO8Llm54+2hJsCCaWVDv+d7txIAku4QZ8kZnUyCjJLG2r1NF+HjpcCk42vuk2P kqag21EK9yVyDDbPmv+FRHS6eME5jSAN+qJ87SJHLe5XTquIq4ZKXJnBMja+W9d66ELe bdic28LSI25205XQXgXCJRCeTF8ysX5tUteG1qnkBmE2pURYFjQG0RQ6R1Yvpv0n9Ejr TJbUeMsYijvwWWhpA2xgRfJ0U5GTziDV/ql9kymAb5hsfvaYBSOdKFaMpzN5WbjDkrMq 7p2g== 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:content-transfer-encoding :mime-version:references:in-reply-to:message-id:date:subject:cc:to :from:feedback-id:sender:dkim-signature; bh=ZmaMH2ATWBsd1xrKMW8MfIDAignemaiSgomNcnLmklE=; b=yHgzZUmo03flRueML2p7CRTjHdohQeFBCXS0SPqWi1+4g5PtrGIWDcjFpoPQV2KMB4 txxu9mBNlbP642DgjY9JSie1UljJtpLdu/A4PloN9S5Md/YEC7YYpE/MiWyHGbDE+u8V crSWhG9OeSqAyltTvvMt49HdWgcAarDg4abvbvorXa4kJm2EODORy5IWPeDDykTOJS08 3ZpKYXgzzio0ww0i0ecVlvSuYfNvy1nW1KF0sWWFRjn6u3u38ZKWDKfhLWzDSxvEkohA 0/o4s9NV3tulsTx3Pc9UjEpMnxXdVNIPOtQm3elju5V9oXja6RsBwlbVPiYqUYPxqH0N Cdcg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm3 header.b=B1flLiEX; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=nHhKFbqT; spf=pass (google.com: domain of jon@jonmsterling.com designates 66.111.4.26 as permitted sender) smtp.mailfrom=jon@jonmsterling.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:content-transfer-encoding:mime-version:references :in-reply-to:message-id:date:subject:cc:to:from:feedback-id:sender :from:to:cc:subject:date:message-id:reply-to; bh=ZmaMH2ATWBsd1xrKMW8MfIDAignemaiSgomNcnLmklE=; b=pQLPN8+xyzjVHORMcH+4xiRfBkmAmyv9OSN32kw+eb+4hJPt4yZ3ffanRswqFy+gkL SREWpwDA/UHN70IDtukhipB/byWBP3TD2gz1Rfl6ypJkiW+TfmU1JaAF6qtGDUcjoze7 799mGxypo6eeOmSh5ceWsDt5y8equBmtpYhCgZGGHKIzUFSTGmfIHUjaHVMUNrYXwKoG lX+7PiEbKtjHwmAtwq5AAzRI5t0Xv3FDrdrAxG4aEajPm53/l71t1gwJJuhR/ivOFToU N55JD92MYHeKZoFyo+DO9/IyG2kVqe/1rUPIZaEtrg6V8K53gsICpAkcMn/IzHm+5KLc GO4Q== 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 :content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=ZmaMH2ATWBsd1xrKMW8MfIDAignemaiSgomNcnLmklE=; b=ECh7U4TKW8AqGJ6wTI7KcbL0HTC/2jkAuvtPgj5Ra5Ermqa6iOTEQxSEZo+Pko8KU9 XzEjH+iE0mv8UL1BekE6zpKnIErxrHOPjwLE9mn+CRaN9hq0Q89Rx5onq4FWsbANWbkO UZdMiTqew72QTe6YZ32q540pnVGHyyJ/ERC2sfwrJi3QEPellUBpQone6tIPy89UoI+W r9o3XBKq11yptOA+WDeBQyVYjv/YbkZ6mUP/Nsaq9uWCRPIHHhhtGaVb7NK+A9f5GrOV 6z8DvogHrCvgkUqr0zHnd2sRzQ2cs67Tvkg9x/I02huPMVPRAc8h+9vKjePEJroXbdQ0 MdSQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AFqh2kofy8o1OhvgwuWILw/cafHfzRFeAbQxa+My1B8YiWyRgIGndJT8 sj9ylPv46FJqaokaX7XdZf0= X-Google-Smtp-Source: AMrXdXuiAbd9ZTaOSccAFd+5sJsWi8IFJZaVBdbWGBp7fsCHITuMFI14NlRxkgxxStVqw4U3WTxbIw== X-Received: by 2002:a25:f02:0:b0:703:7a54:1eb4 with SMTP id 2-20020a250f02000000b007037a541eb4mr3730965ybp.92.1672783571181; Tue, 03 Jan 2023 14:06:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:a067:0:b0:77f:4194:3ddc with SMTP id x94-20020a25a067000000b0077f41943ddcls11077783ybh.4.-pod-prod-gmail; Tue, 03 Jan 2023 14:06:09 -0800 (PST) X-Received: by 2002:a25:50c2:0:b0:75b:4c65:cf30 with SMTP id e185-20020a2550c2000000b0075b4c65cf30mr46837301ybb.7.1672783569510; Tue, 03 Jan 2023 14:06:09 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1672783569; cv=none; d=google.com; s=arc-20160816; b=bsL325wT1l25DPlQDt54UmfBUNJhLyxuB4qxBp9UcLRog0sBvgTvHw/fJZ/2kX7DAT vyI6SkNp/+qT3yLnGwmhOrg2AIGHdjI1N0kvCNGDWk0f9hV+IAu1ZUKyRHIyfiqwwX7V 4QBfX8iuToYmsRDbSpEEAbUvFJpdhyp7GsNTKr0BQONb1ZiwuROwnFTA8xZF+aID6drt AZDBkUmORQtl7mEy4SeQC8aGdSJ6vfvH/3sTnwYiioqfFio67VaI72zFZMjr6HjqjeHf Dq+Yb11QAaWdo+ZJxjjgkf9TQFUjrAX3c4xZPfAncmuq9nlQpqfZw97oz+eY0c2KNRHj QrAQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:dkim-signature :dkim-signature; bh=BKv2sIBnYyP+8WOrAsW5qJDu8BM4MSyMkw5vFUBFMvs=; b=waiLJ3jh4AMixMM3XY9dApBcubmGK2folK2u0UA0owgR5twUJC4PpIZFHLjC5SybeP EcNqKAMYFpOMTb3gwZfIESQdqvVAtIPeGSvIYUGfsO7VVXaTfwKFk61DMlC9rSXLDLzd ZgZYv3lJKOSTEZQdacWWLnIMHSy5Rb0w3NTJUAlZSn1u9mRez71nnFUBqgnN8y9AdOBg kixvuRin0JusBBDMCllwtLyvApti+rVHdXviyKvGNIjg+ZiPPJlO9ISmx75X/ePdsPBq RV24RSh3fTnKO5zceEysMkuhhTrQtRjSwLAgwAg+4u7/zqCLP1s1M08D/YJWOMMCVa0i KlDw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm3 header.b=B1flLiEX; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=nHhKFbqT; spf=pass (google.com: domain of jon@jonmsterling.com designates 66.111.4.26 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Received: from out2-smtp.messagingengine.com (out2-smtp.messagingengine.com. [66.111.4.26]) by gmr-mx.google.com with ESMTPS id p22-20020a25d816000000b006f06d30ef91si2725577ybg.1.2023.01.03.14.06.09 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 03 Jan 2023 14:06:09 -0800 (PST) Received-SPF: pass (google.com: domain of jon@jonmsterling.com designates 66.111.4.26 as permitted sender) client-ip=66.111.4.26; Received: from compute4.internal (compute4.nyi.internal [10.202.2.44]) by mailout.nyi.internal (Postfix) with ESMTP id 1F8725C003F; Tue, 3 Jan 2023 17:06:09 -0500 (EST) Received: from mailfrontend1 ([10.202.2.162]) by compute4.internal (MEProxy); Tue, 03 Jan 2023 17:06:09 -0500 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvhedrjeeggdduheeiucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmne goufhushhpvggtthffohhmrghinhculdegledmnecujfgurhephffvvefufffokfgjfhgg tgfgsehtqhhmtdertdejnecuhfhrohhmpeflohhnucfuthgvrhhlihhnghcuoehjohhnse hjohhnmhhsthgvrhhlihhnghdrtghomheqnecuggftrfgrthhtvghrnhepfeekgfevhfeg gfefgfekfeduueeggeejvddtvdfgteffgfeuleelgeehleefgeejnecuffhomhgrihhnpe gtmhhurdgvughupdgrrhigihhvrdhorhhgpdhgohhoghhlvgdrtghomhenucevlhhushht vghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhrohhmpehjohhnsehjohhnmhhsth gvrhhlihhnghdrtghomh X-ME-Proxy: Feedback-ID: if544409e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Tue, 3 Jan 2023 17:06:07 -0500 (EST) From: Jon Sterling To: Urs Schreiber Cc: Egbert Rijke , Homotopy Type Theory Subject: Re: [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv Date: Tue, 03 Jan 2023 23:05:54 +0100 X-Mailer: MailMate (1.14r5895) Message-ID: In-Reply-To: References: MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm3 header.b=B1flLiEX; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=nHhKFbqT; spf=pass (google.com: domain of jon@jonmsterling.com designates 66.111.4.26 as permitted sender) smtp.mailfrom=jon@jonmsterling.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: , 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 y= our old notes provided an excellent reference. Of course, perhaps this leav= es 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 wrote: >> >> Dear homotopy type theorists, >> >> My textbook Introduction to Homotopy Type Theory is finished and availab= le on the ArXiv: >> >> https://arxiv.org/abs/2212.11082 >> >> From the abstract: >> This is an introductory textbook to univalent mathematics and homotopy t= ype theory, a mathematical foundation that takes advantage of the structura= l nature of mathematical definitions and constructions. It is common in mat= hematical practice to consider equivalent objects to be the same, for examp= le, to identify isomorphic groups. In set theory it is not possible to make= this common practice formal. For example, there are as many distinct trivi= al 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 m= athematics that accommodates the univalence axiom. This, however, requires = us to rethink what it means for two objects to be equal. This textbook intr= oduces the reader to Martin-L=C3=B6f's dependent type theory, to the centra= l concepts of univalent mathematics, and shows the reader how to do mathema= tics from a univalent point of view. Over 200 exercises are included to tra= in the reader in type theoretic reasoning. The book is entirely self-contai= ned, and in particular no prior familiarity with type theory or homotopy th= eory 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 Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeCh= xg%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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/CA%2BKbugeyU16TCLH9MbiBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODH= A%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/B7706C57-2DE8-4AB6-A50B-89F7E6C1067D%40jonmsterling.com.