From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.156.9 with SMTP id f9mr9535047vke.2.1510609244381; Mon, 13 Nov 2017 13:40:44 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.159.62.77 with SMTP id c13ls3639234uaj.18.gmail; Mon, 13 Nov 2017 13:40:43 -0800 (PST) X-Received: by 10.31.156.9 with SMTP id f9mr9535036vke.2.1510609243363; Mon, 13 Nov 2017 13:40:43 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1510609243; cv=none; d=google.com; s=arc-20160816; b=A5qhcEva5xKd3+R9Gw7CUCmMbAD/SAm/rvuU/tDYNjkB47wwmbFLHvd9JrHLEdIc6P WypfpSksZX38nodtkE0i9mpA3mno93TBK04zk5cbduQeDP1eEIlp4+HtKCnJiX5ZSq/m YEWM9u+TAEXq5qNIO1Isz7hggQJM9D2B6F2tHXImeb6b255gy9tdc4mXnyllNWNC49R7 2RTA+5iysIb4gj2u1+fxJcylDCVAFOKwlYjNcqJtYcHLKDHpg/a/wG2I4eeAH6W8YjXS P9MeZdoP0R70FyEC+dSrFrMcZyOsWSEVArlrP3qUWS3j9n5ON3dQ/V9QEqUUXCh3heSk CRNw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:mime-version:user-agent:date:message-id :subject:from:to:dkim-signature:arc-authentication-results; bh=dgSo1AlPXw2h9ItdzUC9kBHwv8f1fNgmIOlMxVnwQ6Y=; b=zK9Yqig74KfwxZm6f8kFPRdzxDN5oja3hwTcCVm7AXZNHHZoeQrBeitnwGOr5B/gUs rAvFxwm8Ggs9/1XEZB0D7J2J5Z2iHugs1Wysn/sTDiX+e68fHn1c/9LyCgFj1BWGXWMr OZsko8WRKU9mXhiwyYzvacFwZwQf9n4IUUeQ0Jr0c/pWX6CZQXvjikzFWEtMukGzCv2D RUVxLY0TEoQCQLzSaCZdy9n9/Bobbx8AD/GVUSTLYLPOkHFDjLCi35rlYOwM9lK8XY3e up5+vleyRAbIgRs1xKbhSq8OIrU22KqWd5PRPss2JbbajnH/2mt0J1fgDbUYWGdHP7z2 Ta7A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@wesleyan.edu header.s=wesgmail header.b=ES62p3Au; spf=pass (google.com: domain of emore...@wesleyan.edu designates 2607:f8b0:400d:c0d::230 as permitted sender) smtp.mailfrom=emore...@wesleyan.edu Return-Path: Received: from mail-qt0-x230.google.com (mail-qt0-x230.google.com. [2607:f8b0:400d:c0d::230]) by gmr-mx.google.com with ESMTPS id y25si583507uaa.2.2017.11.13.13.40.43 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 13 Nov 2017 13:40:43 -0800 (PST) Received-SPF: pass (google.com: domain of emore...@wesleyan.edu designates 2607:f8b0:400d:c0d::230 as permitted sender) client-ip=2607:f8b0:400d:c0d::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@wesleyan.edu header.s=wesgmail header.b=ES62p3Au; spf=pass (google.com: domain of emore...@wesleyan.edu designates 2607:f8b0:400d:c0d::230 as permitted sender) smtp.mailfrom=emore...@wesleyan.edu Received: by mail-qt0-x230.google.com with SMTP id y5so5162660qtk.4 for ; Mon, 13 Nov 2017 13:40:43 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=wesleyan.edu; s=wesgmail; h=to:from:subject:message-id:date:user-agent:mime-version :content-transfer-encoding; bh=dgSo1AlPXw2h9ItdzUC9kBHwv8f1fNgmIOlMxVnwQ6Y=; b=ES62p3Auo8i415SyZwA5nsgFDewPvgIxvuCw4ivjGe0KrWMPd31Rx4kdldVYPaI+HM jEQVc/qx2WdrR99bS7nv5d/X82osFeXMLieRW+Mq2I2ELsPdl5/a9ozOJguuuZDED7sG gUHOz9/hlqynaSw8mgxnz0KeJNdpotaSKYOD8= X-Gm-Message-State: AJaThX5qJa7n49h1lubm8VP5GjajvjlRwBXUTOuI8+Vdw4cTuo5eaWfD VIzg6usmFxMP0k+Ji3fGcJJtXMdftPI= X-Received: by 10.200.22.110 with SMTP id x43mr16848567qtk.278.1510609242871; Mon, 13 Nov 2017 13:40:42 -0800 (PST) Return-Path: Received: from espresso.wireless.wesleyan.edu ([129.133.181.236]) by smtp.gmail.com with ESMTPSA id q32sm11672432qtg.61.2017.11.13.13.40.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 13 Nov 2017 13:40:42 -0800 (PST) To: Homotopy Type Theory From: Ed Morehouse Subject: AMS Special Session on Homotopy Type Theory at the JMM Message-ID: <693531f8-1d78-f7e1-2bb3-734f5cbbb291@wesleyan.edu> Date: Mon, 13 Nov 2017 16:40:40 -0500 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Please accept our apologies if you receive multiple copies of this announcement from different venues. We are pleased to announce the AMS Special Session on Homotopy Type Theory, to be held on January 11, 2018 in San Diego, California, as part of the Joint Mathematics Meetings (to be held January 10 - 13). Homotopy Type Theory (HoTT) is a new field of study that relates constructive type theory to abstract homotopy theory. Types are regarded as synthetic spaces of arbitrary dimension and type equality as homotopy equivalence. Experience has shown that HoTT is able to represent many mathematical objects of independent interest in a direct and natural way. Its foundations in constructive type theory permit the statement and proof of theorems about these objects within HoTT itself, enabling formalization in proof assistants and providing a constructive foundation for other branches of mathematics. This Special Session is affiliated with the AMS Mathematics Research Communities (MRC) workshop for early-career researchers in Homotopy Type Theory organized by Dan Christensen, Chris Kapulkin, Dan Licata, Emily Riehl and Mike Shulman, which took place last June. The Special Session will include talks by MRC participants, as well as by senior researchers in the field, on various aspects of higher-dimensional type theory including categorical semantics, computation, and the formalization of mathematical theories. There will also be a panel discussion featuring distinguished experts from the field. Further information about the Special Session, including a schedule and abstracts, can be found at: http://jointmathematicsmeetings.org/meetings/national/jmm2018/2197_program_ss14.html. Please note that the early registration deadline is December 20, 2017. If you have any questions about about the Special Session, please feel free to contact one of the organizers. We look forward to seeing you in San Diego. Simon Cho (University of Michigan) Liron Cohen (Cornell University) Ed Morehouse (Wesleyan University)