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, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 17525 invoked from network); 30 Mar 2022 12:46:40 -0000 Received: from mail-ot1-x340.google.com (2607:f8b0:4864:20::340) by inbox.vuxu.org with ESMTPUTF8; 30 Mar 2022 12:46:40 -0000 Received: by mail-ot1-x340.google.com with SMTP id o17-20020a9d5c11000000b005b24a70c275sf11623157otk.10 for ; Wed, 30 Mar 2022 05:46:40 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1648644398; cv=pass; d=google.com; s=arc-20160816; b=oBPKYMcRKkHtKxGVQ6dex6nQSjCr8ZqovndxZPrxof0GELVf2azX7CvvSRPkqXM7yL pTZP82AIAHntyVu2G+tKBYyZJXOpAlycqmiQ8SXM3QQ2XvzNvoskvy7GMX9PirVjDYYy NHJCHgWW4Ap255gemRunz3DLfqhOa9bLOuUlncnHrcRjXfCw2vzaQ5Zpnwik+FMQMpQZ Xi/sxSsKIMUSL8ZkAwWjgVRGbWpa+n3lmSGkz55+udhYKAyBzSUIGa4uzfzUiE4YlYpS E8EwgQ2y2lRBugwMaOR/hSB9WFGxxRRww8BD+PXatue3VMcAp5TqPMaVmyyQEWmonZls z5Ag== 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; bh=DKAVI3dQGkV/uW1laihxPA/Fte+YErhYwn4vls/B4iU=; b=VLG2hLHo1H3SiOEqk7L47JylWkGJM0EirqLG8AErU/nE2wglq3gXA0XiFo4eJ0rskp /C1nxJZr8tWmqIm+DDKL1x8FuHtdJ9bhe6oH6x/Sp69RrJx/kL093EwTxpnqEzgO4ubJ +b8s7UUuPsUDGfg3ve4ONaAm7o2hbHUPOORiPJ1qXnWVqf+Er5yHG88qreRw4RoA7J5Y BbEU1lz6L7Z7OTB9V/0ZQfSzdjd58kLA+sv48B1EUYskqtVzLfeq7pnnsKyuF9OgZ3qr 2VbYdTNh8rqahULqTaLqJlruOvlZ0QsoCU370QleOKlXjNuFMc96ly9o2/paXsh3MSnP 5+qQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@unifi.it header.s=google header.b=SA2X52it; spf=pass (google.com: domain of marco.maggesi@unifi.it designates 2607:f8b0:4864:20::231 as permitted sender) smtp.mailfrom=marco.maggesi@unifi.it DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=DKAVI3dQGkV/uW1laihxPA/Fte+YErhYwn4vls/B4iU=; b=TCybK03LPh871P8iqEY469QHoPIg93yIYdGFbOAWW3ZXBiXJPcU5LddDYOa7iVTEjv UetbO4dQv4gHFfXZL/s842+Mce/fC8xTykApImWIzcL8xlti9v1O72tukzd0zYXTOxnz YUvc4lqFbI65qLm+4Y2Qj/x7+JGwuxy7gQN+ro+eJnfTsoEISClF0kkK3mesEe66Y+ks BUWyQ5L85JUBaAr7b+u6IZYMk2PHPpRq7SKQrMEeqAeDTcoP5GgzG5aM1Sh7C7u7jXer y/F3w4eMK3aB8X9L47Os5ZKyGVeEWp7+hk3j9EaynsoL2/z6NfJRou99b8N601MOj8Ii HrcQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-subscribe:list-unsubscribe; bh=DKAVI3dQGkV/uW1laihxPA/Fte+YErhYwn4vls/B4iU=; b=S0BExIpY5SUc0PXtT4rpVW45YWjUZoHxSdLnkddVkm4wJxw48raOaRyxq95DMQcfLO Wc2iWRGYoFIAEIu6pOvwQGKcHA0aCXRv8sGhXU1yM80oKBqrVgIinc3k1LcGHSL4wO4m VbDPALdzoecoBwjdQPi3Lu7JQbsHlXGqYYHY03JCi9R1XhYwJak4agcufhc5xjSdm7wj z/yfhBpv48Hg62X6/GLNG85fzgrLKYcCQHDBmrdhCvR2sK64MxIek/XdiKxNK+raBlwx FkUXopdFSN2ufJ8SZJlrme4/FV//AW9Yb84UXgg2fclw6MJo+c5HzayYxoGsBU9I3Ev4 lZqw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530+uqfzX3C7zxo25TfgzQxugdAKEE+vWkQ14qV/yt7BK6jFeI6T JbJBUxK6cVcuHGpvHr2lykY= X-Google-Smtp-Source: ABdhPJyjFd7OxlDBBQDbWdNdxz8An2A2Z8HyAWnVDpmqtddZy17Sk/QdJ1PZ8Imbbyv+CWQ2zP+aag== X-Received: by 2002:a05:6870:420c:b0:dd:f2c0:534f with SMTP id u12-20020a056870420c00b000ddf2c0534fmr1963479oac.241.1648644398060; Wed, 30 Mar 2022 05:46:38 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6870:44:b0:df:dc4:2fc0 with SMTP id 4-20020a056870004400b000df0dc42fc0ls793187oaz.11.gmail; Wed, 30 Mar 2022 05:46:37 -0700 (PDT) X-Received: by 2002:a05:6870:a788:b0:de:c1c1:ac07 with SMTP id x8-20020a056870a78800b000dec1c1ac07mr1987090oao.68.1648644397088; Wed, 30 Mar 2022 05:46:37 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1648644397; cv=none; d=google.com; s=arc-20160816; b=nH3uYiXOScVyF6htBy/8JjNbyfxYamhUD385N+G95ndaBZVzG2drc9nm9JQnjGx+dW TrVL7zA0+TmQnPDzHp8ci22CHeh4rK5Ux+dFbZmH9ZRRVCqOgZZ0i0JvDzd6piwtrPPB aGNdje0otZPn1NS9i3isYvspU+ZsrAja6ezHvkwJ7mbvLNHYr/0joRufVtSLopg28LNZ M+OGn0gVKvljeS21LtZwoDpL64nBmQdxx5O9GSBJVYxTWlfEnIZ2HtZcV3/si5BaKE5m 9oCTGFjYegv3L8k5BXWvTR/XJmFdpsPVdQx4CLqB++7fIWI8X1q18MNaKEeSfkDHKeY9 9dqw== 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=5n4ed+ZY9FxCOmj8b18m0oawxrboYHEziXdyU86QKQE=; b=QWZmTX6OMXNw0klTFCfbZEo9ioUNlNelqgmzNhukibOCtze1x7kgjsNA1BRFpPp8VP RTEL/2OKO6nUIHfk+PmoTxGQ3L9wRqAyqapo0jGp4QEDiCUVSVdWa08E84V3bkxUPvpG Up+FxKkavpmKRMa3IEMVQP5/Bt7lQK30fS2XS03CkUd61T2GC688JPA+kTo8+wljliYI erbjz5ClX5QWV3yGybXYMq1cKihUXlcYORt96vkK0erK71ygYi6IYMBOfYI0zR7uFRzz ARGfawtcqflhp4KPh+FGCdte+vIJ5uDKg6xCEcZB8fjsbmF6yE8yGLyTDpZmTj/dXVxV 9YtQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@unifi.it header.s=google header.b=SA2X52it; spf=pass (google.com: domain of marco.maggesi@unifi.it designates 2607:f8b0:4864:20::231 as permitted sender) smtp.mailfrom=marco.maggesi@unifi.it Received: from mail-oi1-x231.google.com (mail-oi1-x231.google.com. [2607:f8b0:4864:20::231]) by gmr-mx.google.com with ESMTPS id t17-20020a05687044d100b000df1b6357aasi504514oai.5.2022.03.30.05.46.36 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 30 Mar 2022 05:46:36 -0700 (PDT) Received-SPF: pass (google.com: domain of marco.maggesi@unifi.it designates 2607:f8b0:4864:20::231 as permitted sender) client-ip=2607:f8b0:4864:20::231; Received: by mail-oi1-x231.google.com with SMTP id v75so21976229oie.1 for ; Wed, 30 Mar 2022 05:46:36 -0700 (PDT) X-Received: by 2002:a05:6808:140b:b0:2ec:f41e:a4c6 with SMTP id w11-20020a056808140b00b002ecf41ea4c6mr1608126oiv.17.1648644396415; Wed, 30 Mar 2022 05:46:36 -0700 (PDT) MIME-Version: 1.0 From: Marco Maggesi Date: Wed, 30 Mar 2022 14:46:25 +0200 Message-ID: Subject: [HoTT] School on Univalent Mathematics, Cortona (Italy), July 17-23: Application deadline 15 April To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000009c10d605db6eef6b" X-Original-Sender: marco.maggesi@unifi.it X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@unifi.it header.s=google header.b=SA2X52it; spf=pass (google.com: domain of marco.maggesi@unifi.it designates 2607:f8b0:4864:20::231 as permitted sender) smtp.mailfrom=marco.maggesi@unifi.it 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: , --0000000000009c10d605db6eef6b Content-Type: text/plain; charset="UTF-8" We are pleased to announce the School on Univalent Mathematics 2022, to be held at the Palazzone di Cortona (https://www.sns.it/en/palazzone-di-cortona), Cortona, Italy, July 17-23, 2022 (https://unimath.github.io/cortona2022/) Overview ======== Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky's program of Univalent Foundations, a new approach to foundations of mathematics based on ideas from homotopy theory, such as the Univalence Principle. The UniMath library is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is based on the computer proof assistant Coq. In this school, we aim to introduce newcomers to the ideas of Univalent Foundations and mathematics therein, and to the formalization of mathematics in UniMath (https://github.com/UniMath/UniMath), a library of Univalent Mathematics based on the Coq proof assistant. Format ======= Participants will receive an introduction to Univalent Foundations and to mathematics in those foundations. In the accompanying problem sessions, they will formalize pieces of univalent mathematics in the UniMath library. Prerequisites ========== Participants should be interested in mathematics and the use of computers for mathematical reasoning. Participants do not need to have prior knowledge of logic, Coq, or Univalent Foundations. Application and funding ======================= For information on how to participate, please visit https://unimath.github.io/cortona2022. The application deadline is 15 April 2022. Best regards, The organizers Benedikt Ahrens and Marco Maggesi -- 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/CAN%2BOvf%3DqzEd5hhSQycGZKb0EAuNYng3%2B6_z1ghW9M3xpLNx8HA%40mail.gmail.com. --0000000000009c10d605db6eef6b Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
We are pleased to announce the

School on Univalent = Mathematics 2022,

to be held at the Palazzone di Cortona
(https://www.sns.it/en/palaz= zone-di-cortona),
Cortona, Italy, July 17-23, 2022
(https://unimath.github.io/cortona2022= /)

Overview
=3D=3D=3D=3D=3D=3D=3D=3D
Homotopy Type Theory = is an emerging field of mathematics that studies a fruitful relationship be= tween homotopy theory and (dependent) type theory. This relation plays a cr= ucial role in Voevodsky's program of Univalent Foundations, a new appro= ach to foundations of mathematics based on ideas from homotopy theory, such= as the Univalence Principle.

The UniMath library is a large reposit= ory of computer-checked mathematics, developed from the univalent viewpoint= . It is based on the computer proof assistant Coq.

In this school, w= e aim to introduce newcomers to the ideas of Univalent Foundations and math= ematics therein, and to the formalization of mathematics in UniMath (https://github.com/UniMath/UniMath= ), a library of Univalent Mathematics based on the Coq proof assistant.=

Format
=3D=3D=3D=3D=3D=3D=3D
Participants will receive an int= roduction to Univalent Foundations and to mathematics in those foundations.= In the accompanying problem sessions, they will formalize pieces of unival= ent mathematics in the UniMath library.

Prerequisites
=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D
Participants should be interested in mathematics a= nd the use of computers for mathematical reasoning. Participants do not nee= d to have prior knowledge of logic, Coq, or Univalent Foundations.

A= pplication and funding
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D
For information on how to participate, please visi= t https://unimath.github.= io/cortona2022.
The application deadline is 15 April 2022.

Be= st regards,
The organizers Benedikt Ahrens and Marco Maggesi

--
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/CAN%2BOvf%3DqzEd5hhSQycGZKb= 0EAuNYng3%2B6_z1ghW9M3xpLNx8HA%40mail.gmail.com.
--0000000000009c10d605db6eef6b--