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,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 18937 invoked from network); 23 Dec 2022 14:22:58 -0000 Received: from mail-io1-xd3e.google.com (2607:f8b0:4864:20::d3e) by inbox.vuxu.org with ESMTPUTF8; 23 Dec 2022 14:22:58 -0000 Received: by mail-io1-xd3e.google.com with SMTP id o22-20020a6b5a16000000b006e2d564944asf1933727iob.7 for ; Fri, 23 Dec 2022 06:22:58 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1671805376; cv=pass; d=google.com; s=arc-20160816; b=Kmub9cS9mZJWgXwhP7sTujxDY/QYY9r05SP3hfjW5hkEMahHaE2bznHoIIXkya6r/2 FRJdX6zPnu03dgGXdhy8OedPY1xMogets8bc9zJUKg2garhh0U+9FXY5uDHODZay/F0L JArCvNVM4ps390CQjoBICD1wmC0YH0DVnIkJr66KiKSLAEe1mGd9/IJpRQW2+Z1qe++K +9e2krbEzfW86IE0Ath6LHfNFMeKS0KgI7Fd6vsJBLgp/XO4D4WF65cgbGO1cG+U197Z XgNHfd+Xfhh1EVB/of6/TcomkH5Ts29Ddida/8SXMtVm1Ts7JQ6w/tNKdB266oVOMFh2 70yw== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=d+8CLQG+yt5QPp0QlGpWe5Fyxm6cJSPH5z9H//oJSOQ=; b=1AIHoOjGnF7JP6dhZ5tiqoGXWEGnnEivirqmmmIA3FJ9XBb/Sot4A+Pi5HQwU3D44t nLzLKec7KYzF1p7FVTkru74nxQz4BavC5VMzmuvOxRQ8/y0ag48kwWhqC3IbfoeoMRHE csCWYX/sYDhM2g1hkWXOv5lqFE5qo6SV5ZIy6SKNgj7KxFRB4Rgz7ki+diY8CoN/UrqA Wnj85/qEW/u2l8MGkKsFF3yjijYuKjkTpCboOnQ0C/8x26yPd3lbyMjyzNbiqax3xtg5 qFfXub/PiPn+kkrawA2sn+l8ah0aCwAcpg6hzRSP4hW3Hp5dKcJNJM4l2wA6fvIpnJmI boQw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@dmat.ufpe.br header.s=google header.b=e7A7mvHG; spf=pass (google.com: domain of jasj@dmat.ufpe.br designates 2607:f8b0:4864:20::12d as permitted sender) smtp.mailfrom=jasj@dmat.ufpe.br; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=dmat.ufpe.br 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:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=d+8CLQG+yt5QPp0QlGpWe5Fyxm6cJSPH5z9H//oJSOQ=; b=kSmuSIIbrPEB+wQf1lR6HyL55nGyTzIFEQAgPnsAgWORYBxS/WYJjLHEW+5zF8uVFO snNHYbSX6Uppcwc6djmcFkEdS/8MbEM1hzTCt3HdKAcdL+48mm4wBfZMyXbvq9cRPol/ vNUqeh6xUj6Zan1goPEDdBmFfzJ0d5r3CcWPLJaaGdnZcDULeOV5bzoLLohZEok2jBR+ wRlXSMQkTh46BLu4qBEZrpUf2pQ543AlVockJKRElQnKrnztU1FHQjpSVg1zSVGmcy66 QGfhKBn7CgYOa5nr7gTovZ4F2REcECK6zRX8+pEbj2M+bC+onasuqsknZasIdPKPs+xU 8QXg== 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:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=d+8CLQG+yt5QPp0QlGpWe5Fyxm6cJSPH5z9H//oJSOQ=; b=jUMhKPXZPfFIzOLlfcGKu91AK7vOazgqmB5OpdQFbYTeosyiZyMkh+X4OUB9/cUDye JL8xFZ+EIdqKEgZYaTad3Nb72Cb19TVrxXzTcJ8OCPaXO5ZQclK9cGzboHZvJHIYhq+A XqfZPalum5cK3MOeJ3KEfV18EsoY74IQXm1dl1zSs+VUecKq7GKHrp9FnupcLhHPWJsH E4EhQjB32MConuFZKoQEbOre/dlkkSa1Oz0qCFD+Y2qIDM2UxdRh30daXRWQBviccVZJ ZKo1X0+Z4m9SQ5HzZqBxbGPaehAsg3sf+0ZmDpMCrD3tLEPEkcttNPEadM1o/BJI3Ilr uR1g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AFqh2kqiUb3PFTSg9Iuojk2E68Svq9zmzEuzGhck1uMpS2JBsneAqQcr DZwWTjk2B6lfJ0eQzYHhF1w= X-Google-Smtp-Source: AMrXdXvzt6/a1IaZgb775VxoyQvybghqF/0Yd0J9572gYHaHBWa/HDJLWDXKb8P8MNrcdamVBfKWTA== X-Received: by 2002:a02:c601:0:b0:38a:93f7:4f65 with SMTP id i1-20020a02c601000000b0038a93f74f65mr798468jan.16.1671805376171; Fri, 23 Dec 2022 06:22:56 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6e02:c73:b0:30b:e84d:f8ea with SMTP id f19-20020a056e020c7300b0030be84df8eals523942ilj.9.-pod-prod-gmail; Fri, 23 Dec 2022 06:22:55 -0800 (PST) X-Received: by 2002:a05:6e02:14cf:b0:30b:d94a:a4f5 with SMTP id o15-20020a056e0214cf00b0030bd94aa4f5mr6994247ilk.7.1671805375122; Fri, 23 Dec 2022 06:22:55 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1671805375; cv=none; d=google.com; s=arc-20160816; b=TPOn0qpHzLMeGOnq7A+VOTKz5EhYUAvRoVqfiPNZpMJD2gKQEgEi9wUGQbnUpYmmxD zPVPOSSmzuWDBpJy5eg+vxU9sAU4ytPLNdvyQj4SGVeGxw3Qb1s9ZTIMi3AJ8kzyb+EK v+RzXpPzeqaNu+SM3AgJmwKNNhRhOHm0BcrWfk7uxZYJurnSEbVrUsJkujhNh7k6JypW L7wkHCDmrg1aeMMmpJAvG0ZUL8KRG4VZ3rjsqn/5ZiQK3wr6QKJGvgskYhEO+nHFRYW6 HKi221MIGt96fI4mLpFIMUQKWxxILHgj2Gax3x1vnjYWpzERyUZNae5nP85VeMXgMH02 9Onw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=yBSqkS5AT090czjFe/egiywNJafiTQ1NXGsoMw32LUc=; b=OxOYIDUXZllMeGKsMjY0L/y0SMlSmaV9l+lM4mIeZsdeoAdka24WeqhPHljp5sgitC GsUKzYkxWfBWmn9AW574ahxDQNenS1hiW8ipvhP/Of/zvp5YhXqKIcTE7EONMpn6h4nb y+zTq2eNlSYcXagYraS2RHcwV+eqZerR3LJdWBoHOZXQE2qHYUwUk9lP9/PxAjkrlmgj 38Y7+WjCCeKs0BEoMWX6iULtzsy2SYmKv3z244lf0B3d4bHPOr+eQh5jzmzxrgdtZJv2 MoKwuJca9uK9MjB6X28C2o5pFEJy7zkoImEECK/MYMzEdjTA37vSZoZwGsSZ2CYunoj7 +x6g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@dmat.ufpe.br header.s=google header.b=e7A7mvHG; spf=pass (google.com: domain of jasj@dmat.ufpe.br designates 2607:f8b0:4864:20::12d as permitted sender) smtp.mailfrom=jasj@dmat.ufpe.br; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=dmat.ufpe.br Received: from mail-il1-x12d.google.com (mail-il1-x12d.google.com. [2607:f8b0:4864:20::12d]) by gmr-mx.google.com with ESMTPS id c9-20020a02c9c9000000b0038a6bbe1e21si300490jap.1.2022.12.23.06.22.54 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 23 Dec 2022 06:22:54 -0800 (PST) Received-SPF: pass (google.com: domain of jasj@dmat.ufpe.br designates 2607:f8b0:4864:20::12d as permitted sender) client-ip=2607:f8b0:4864:20::12d; Received: by mail-il1-x12d.google.com with SMTP id s16so2527812iln.4 for ; Fri, 23 Dec 2022 06:22:54 -0800 (PST) X-Received: by 2002:a05:6e02:c88:b0:303:e37:21f1 with SMTP id b8-20020a056e020c8800b003030e3721f1mr737036ile.243.1671805374413; Fri, 23 Dec 2022 06:22:54 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: =?UTF-8?Q?Jo=C3=A3o_Alves_Silva_J=C3=BAnior?= Date: Fri, 23 Dec 2022 11:22:45 -0300 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: multipart/alternative; boundary="00000000000079d9be05f07f85e5" X-Original-Sender: jasj@dmat.ufpe.br X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@dmat.ufpe.br header.s=google header.b=e7A7mvHG; spf=pass (google.com: domain of jasj@dmat.ufpe.br designates 2607:f8b0:4864:20::12d as permitted sender) smtp.mailfrom=jasj@dmat.ufpe.br; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=dmat.ufpe.br 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: , --00000000000079d9be05f07f85e5 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thank you! Em sex., 23 de dez. de 2022 06:54, Egbert Rijke escreveu: > 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 > 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 singleto= n > 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 > 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. T= he > 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/CAGqv1ODuH3xtsFyFEek= jwNH4SUN%2BdU8B1te2ZLX%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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CABUO1-ihPx2Zugxh9YbWA626Dc4uyQuaCtrxvHTGuLog%2Bza49g%40= mail.gmail.com. --00000000000079d9be05f07f85e5 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thank you!

Em sex., 23 de dez. de 2022 06:54, Egbert Rij= ke <e.m.rijke@gmail.com> e= screveu:
Dear homo= topy type theorists,

My textbook Introduction to Homotopy Type Theor= y is finished and available on the ArXiv:

https://arxiv.org/a= bs/2212.11082

From the abstract:
This is an introductory text= book to univalent mathematics and homotopy type theory, a mathematical foun= dation that takes advantage of the structural nature of mathematical defini= tions and constructions. It is common in mathematical practice to consider = equivalent objects to be the same, for example, to identify isomorphic grou= ps. In set theory it is not possible to make this common practice formal. F= or example, there are as many distinct trivial groups in set theory as ther= e are distinct singleton sets. Type theory, on the other hand, takes a more= structural approach to the foundations of mathematics that accommodates th= e 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 theory, to the central concepts of univalent m= athematics, and shows the reader how to do mathematics from a univalent poi= nt of view. Over 200 exercises are included to train the reader in type the= oretic 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!

Happ= y 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@googleg= roups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/Homotop= yTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CABUO1-ihPx2Zugxh9YbWA626Dc4uyQ= uaCtrxvHTGuLog%2Bza49g%40mail.gmail.com.
--00000000000079d9be05f07f85e5--