From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x23f.google.com (mail-oi1-x23f.google.com [2607:f8b0:4864:20::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b8f15ea8 for ; Wed, 12 Feb 2020 17:21:37 +0000 (UTC) Received: by mail-oi1-x23f.google.com with SMTP id 199sf1294222oie.10 for ; Wed, 12 Feb 2020 09:21:37 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=V4Fan0Mdsdinv/b2KM84bJXtRlZBVJZmAzx1vfGeZSs=; b=FhMh+yN5dHXxyfzJ06e6uuEvWxeq+t3IBmJow2JtfF/+Ro+X4+kxt6cHZL7xbBzQ9K stV/NzSW5gkkO2+wdkP47qMlWqQKPtbL3MWGZMTRdTm+4Dp1+5oprYsWoKPsOdnrFYfM vbebX5nuOCCnaElwr4xWqIGx5IGpXHpz5yX7T48EarIa7tPpGCrUuudi9kTl4W26BFTj Nyys4ypzPgXS7Z10AnI2V+9OvELXv/IAuUTBq2DDHVFQ+eL9OrOM1kFBw+h07qUqtKyg hnpTWYQ32giWVDofYpns5j3QOlXexNmmYuMgA+qmwS3dkm9P4xZzHiwvs25cv4hputnJ yFgQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=V4Fan0Mdsdinv/b2KM84bJXtRlZBVJZmAzx1vfGeZSs=; b=lNquzI4AwvK15Bw3i1j446weJFIwu8OExy9VouN1Y7VrpETuZByY55L9PKWjI7kPoE kL/U9WoeFJfQiJHG9gxC7CQLbebq6r7f3BEZMpp6LmN0VNlhbtbW86OO/XaCF1hdPzGz l2l6Pqzs5NxbiO6BIWKU5nXYHTmuqecgC8aR4UbFdYf5st7AWcnJhYZVq4tAui8Ric+E Xb9fTl0dAU1b0OWC/n1pyBi2i+sQIwnuQkvbt9vtz0XdgorTRJHB8b3EmmLbSQT3PW00 jNRE8ZyOAo38TChuiNED3FKU+PR9AWow8Z/3wZmfhXvXAf/DlEctxrv6co74rfPtayDx 5i5A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=V4Fan0Mdsdinv/b2KM84bJXtRlZBVJZmAzx1vfGeZSs=; b=GyHjaSMwdfJnho+fx8y33xu82EY2Ll1cuk6nCai3brRCvMNnPiuE7HD+e7hAe77gF+ VRIrjzKN+a9CfYlGbKmy0DyKFhOkepbgMJuIWD0xn4OVgqNNIKYH4DYnO92McXr+HuMG c3eutC3qM4IbK7O53MqIMiCrVuQFxrUYNm6wxoW7SsTudxsClB14jMcmAwVnpuEdpP57 s+Ef8Lkt6tkVkJnUPVCkpRiPvP187ATZNQLLqLZCTvIKGLr2VbL0usaNyJt5EageP7ji vdl9CgWEIJ1HhjtgUR90P+OtOww+5udjZWrHb3ST9LgnIXhn2evOiUwvuyTsMoF4HCE2 OgiA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWS8f0YepUaRcSy5Bqbqu4KaH64v2ihgUFS0S50KCnk76k81Y6J 8yDhKdfm2Ve4ihw+be+RRWo= X-Google-Smtp-Source: APXvYqyuuepoedFIqY5BCSbiCl9jgl4A16bCZD/kbdyGlEQWL1UASz+JhSoMvHlv2vUYOeOUapGlPQ== X-Received: by 2002:a05:6830:13ca:: with SMTP id e10mr3639230otq.267.1581528096070; Wed, 12 Feb 2020 09:21:36 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:5a87:: with SMTP id w7ls4691883oth.1.gmail; Wed, 12 Feb 2020 09:21:35 -0800 (PST) X-Received: by 2002:a9d:3b3:: with SMTP id f48mr3374832otf.148.1581528095082; Wed, 12 Feb 2020 09:21:35 -0800 (PST) Date: Wed, 12 Feb 2020 09:21:34 -0800 (PST) From: Marco Maggesi To: Homotopy Type Theory Message-Id: Subject: [HoTT] School on Univalent Mathematics 2020, Cortona (Italy), July 27-31, 2020 MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2590_1989351156.1581528094468" X-Original-Sender: marco.maggesi@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: , ------=_Part_2590_1989351156.1581528094468 Content-Type: multipart/alternative; boundary="----=_Part_2591_619856932.1581528094468" ------=_Part_2591_619856932.1581528094468 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable We are pleased to announce the School on Univalent Mathematics 2020, to be held at the Palazzone di Cortona (https://www.sns.it/en/palazzone-cortona), Cortona, Italy, July 27-31, 2020 (https://unimath.github.io/cortona2020/) Overview =3D=3D=3D=3D=3D=3D=3D=3D 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 and workshop, we aim to introduce newcomers to the ideas of Univalent Foundations and mathematics therein, and to the formalization of mathematics in a computer proof assistant based on Univalent Foundations. Format =3D=3D=3D=3D=3D=3D=3D Participants will receive an introduction to Univalent Foundations and to mathematics in those foundations, by leading experts in the field. In the accompanying problem sessions, they will formalize pieces of univalent mathematics in the UniMath library. More information on the format is given on the website https://unimath.github.io/cortona2020 . Application 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 visit https://unimath.github.io/cortona2020/. Mentors =3D=3D=3D=3D=3D=3D Benedikt Ahrens (University of Birmingham) Joseph Helfer (Stanford University) Tom de Jong (University of Birmingham) Marco Maggesi (University of Florence) Ralph Matthes (CNRS, University Toulouse) Paige Randall North (The Ohio State University) Niccol=C3=B2 Veltri (Tallinn University of Technolog) Niels van der Weide (University of Nijmegen) Best regards, The organizers Benedikt Ahrens and Marco Maggesi --=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/ddefa71a-42c0-4abf-8b73-8f2a980f948d%40googlegroups.com. ------=_Part_2591_619856932.1581528094468 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
We are pleased to announce the

School on Univalent Mathematics 2020,

to be hel= d at the Palazzone di Cortona
C= ortona, Italy, July 27-31, 2020
Overview
=3D=3D=3D=3D=3D=3D=3D=3D
Homotopy= Type Theory is an emerging field of mathematics that studies
a f= ruitful 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 mathematic= s
based on ideas from homotopy theory, such as the Univalence Pri= nciple.

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

In this school and workshop, we aim to introduce newcomers= to the
ideas of Univalent Foundations and mathematics therein, a= nd to the
formalization of mathematics in a computer proof assist= ant based on
Univalent Foundations.

Form= at
=3D=3D=3D=3D=3D=3D=3D
Participants will receive an i= ntroduction to Univalent Foundations and to
mathematics in those = foundations, by leading experts in the field.
In the accompanying= problem sessions, they will formalize pieces of
univalent mathem= atics in the UniMath library.

More information on = the format is given on the
<= br>
Application 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

<= /div>
Mentors
=3D=3D=3D=3D=3D=3D
Benedikt Ahrens (U= niversity of Birmingham)
Joseph Helfer (Stanford University)
Tom de Jong (University of Birmingham)
Marco Maggesi (Unive= rsity of Florence)
Ralph Matthes (CNRS, University Toulouse)
Paige Randall North (The Ohio State University)
Niccol=C3= =B2 Veltri (Tallinn University of Technolog)
Niels van der Weide = (University of Nijmegen)

Best regards,
T= he 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.co= m/d/msgid/HomotopyTypeTheory/ddefa71a-42c0-4abf-8b73-8f2a980f948d%40googleg= roups.com.
------=_Part_2591_619856932.1581528094468-- ------=_Part_2590_1989351156.1581528094468--