From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.114.76 with SMTP id c12mr4517153pgn.10.1504289729872; Fri, 01 Sep 2017 11:15:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.182.139 with SMTP id g133ls1953886iof.36.gmail; Fri, 01 Sep 2017 11:15:28 -0700 (PDT) X-Received: by 10.36.9.132 with SMTP id 126mr1091057itm.13.1504289728018; Fri, 01 Sep 2017 11:15:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1504289727; cv=none; d=google.com; s=arc-20160816; b=fBTYRuUEepCd2PhwR3kqLWchEHB023c1aP7r7p9frIMEt6ayNYLcpxOCnnqiF8UJxX V4t/PAkhj36zmTE7YSbDukT0L5XHYhr2d1ZqaUT36KB3iXPz6ELGEGfAhuZ/1+lKcTL3 8KaLsgKkYvcalTCnLtimX1e+NSJsQa0EJyDgJGI9cbtMW61DrC6xg8WcROnSXrQSqYYQ Vh24iL7G9E2Xsl/iLiZUDaLRC4iUji45sKR1d5JqlnQaIMlkorQgGmcv1m531wvs/DFx DfSFnBzMe6phJXvMUGb3zDMEqFbRdWJBSaevET64XArQ5f93LwUyOO12ruJaSwByOskh HdGQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature:arc-authentication-results; bh=KyhqDoGh8OVy5EHonueurhTBFkpwn2aGKePYLAqagKM=; b=tt+3tcOdSAzrEVmq9DoRWfT2X+RF4Gqw+/r5VKW4DbPiGsOY14L80f1Z0fkCMtQh1B 1mAX4aGCDrAEKPB3NOQO0uq/aGLf/0w97rQYAuBdkN3bwFfy7ZRM47fERuOc4LyVH+r9 +9B+1gFGFgzCGfup9CVxnLCU67E9DXASCaHaZbR8tfRhKCkcz//FCAP3FHjS11VK3r5U Q0QyWNx3QS33/Pz1/Mqyhjxcx/K5R/KG6j8qalXXlVXBemBiyxCXZ5XLcGf8b/G+Zel1 jCnYt+fI+Ki/0DG4W17U3zRfcd4ProWlFS5voXIvtvsGyyXuPPI/A5UuHzwzIkivrk7y rDxw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=J36o6ee+; spf=pass (google.com: domain of k.kap...@gmail.com designates 2607:f8b0:4003:c06::241 as permitted sender) smtp.mailfrom=k.kap...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-oi0-x241.google.com (mail-oi0-x241.google.com. [2607:f8b0:4003:c06::241]) by gmr-mx.google.com with ESMTPS id p137si40681itb.0.2017.09.01.11.15.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Sep 2017 11:15:27 -0700 (PDT) Received-SPF: pass (google.com: domain of k.kap...@gmail.com designates 2607:f8b0:4003:c06::241 as permitted sender) client-ip=2607:f8b0:4003:c06::241; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=J36o6ee+; spf=pass (google.com: domain of k.kap...@gmail.com designates 2607:f8b0:4003:c06::241 as permitted sender) smtp.mailfrom=k.kap...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-oi0-x241.google.com with SMTP id w10so780254oie.1 for ; Fri, 01 Sep 2017 11:15:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding; bh=KyhqDoGh8OVy5EHonueurhTBFkpwn2aGKePYLAqagKM=; b=J36o6ee+FnefHffNY8fg0cWsRYhQxkYLEMHrP0wXR910Td1GjOyrt1s/+/BnzxJdrT 4AhsHmW8JyX4Rw4NGlh0ZPmNVl1O4TH4qsuKnDufRBqjHzEUDsEbdlDYVB2S6/iIoAF/ asYvjJkmvPYsSHe3fBJyiWuXDRzO6MpRN6WJLxDcPB+vtHKuBkKk3zS/nTveRcoRCyOW fqqdcGmnlQ0n61fJSs3nBfLKJMhnDUBOX/hQeuTgMAQ0pEdEabopkakFi8xWHDxO6Ztt ICqNlxFJl3NwpqzmlSZUExLB4Ibc1B2V7mA5wKd2yF4CodOanv1H6W8eSaoGlN93ujfg 87Ig== X-Gm-Message-State: AHPjjUgjVM5+xyVy/bHwVNQn2RuzeRTNJhJj31e11pdblAQRQbasDOEo wR7/kezfyqJS5BE22AbL3UtrO2JziVyr X-Received: by 10.202.117.129 with SMTP id q123mr2458988oic.16.1504289727485; Fri, 01 Sep 2017 11:15:27 -0700 (PDT) MIME-Version: 1.0 Received: by 10.58.18.159 with HTTP; Fri, 1 Sep 2017 11:15:07 -0700 (PDT) From: Chris Kapulkin Date: Fri, 1 Sep 2017 14:15:07 -0400 Message-ID: Subject: School and workshop on univalent mathematics, 11-15 Dec, Birmingham (UK) To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear all, We are pleased to announce the School and Workshop on Univalent Mathematics to be held at the University of Birmingham (UK), December 11-15, 2017. Overview ---------- Univalent 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. The workshop will give many young researchers an opportunity to familiarize themselves with the UniMath library and become contributors. Format ---------- During the school/workshop, the participants will be working either individually or in small groups, mentored by experienced UniMath developers. The problems will be designed to be of practical importance in the development of the UniMath library as well as of pedagogical value to participants. Application and funding ---------- For information on how to participate, please visit https://unimath.github.io/bham2017/. The deadline to apply is October 15, 2017. Financial support is available to cover participants' travel and lodging expenses. Mentors ---------- Benedikt Ahrens (University of Birmingham) Mart=C3=ADn Escard=C3=B3 (University of Birmingham) Daniel Grayson (University of Illinois Urbana-Champaign) Joseph Helfer (Stanford University) Kuen-Bang Hou (Favonia) (Institute for Advanced Study, Princeton) Chris Kapulkin (University of Western Ontario) Peter Lumsdaine (Stockholm University) Ralph Matthes (CNRS, University Toulouse) Vladimir Voevodsky (Institute for Advanced Study, Princeton) Matthew Weaver (Princeton University) Best regards, Benedikt Ahrens and Chris Kapulkin for the organizers