From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.37.188.145 with SMTP id e17mr1263466ybk.57.1507268489560; Thu, 05 Oct 2017 22:41:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.129.182.40 with SMTP id u40ls1411658ywh.43.gmail; Thu, 05 Oct 2017 22:41:28 -0700 (PDT) X-Received: by 10.129.12.131 with SMTP id 125mr823726ywm.123.1507268488727; Thu, 05 Oct 2017 22:41:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507268488; cv=none; d=google.com; s=arc-20160816; b=Lukew/y22qkUX6LJQtsoeOjZ9MTB3fRCEyV5nKpkBkpiZG6y9b7/4cdHaCaekPkzml 2cVWmFObIMoC243NTusqf/JlKGT16LEkdLxAA3/n4rZZbPsdLdJA8o82TOGijJhiTebI 5zjWdjdyVCoGkq69fCwwp2PoiHoltnaw1L1zfw13b1GSrodl5RRfN6yk0eBnvPgYtvK4 XAVjYnzUrte/z+vMbkOqRpc1IiGSjkyjKRXOmKL0bScW/2BzzGvLPrikApZOPlxwVBee 1wRbilS1SOELtV7BD0biy/5WAEHzw/hPOJHNCRTfSObpRYDnwcyXa14zEkaKp3OFks8x WmOw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=Q1kV/u3Oz3HZd4IzQ22WH62pmEoJGkXf2Mzta0ykW4A=; b=rEURlYsq1CHZijZHYyBvhg3fFNWcLrzNFPqv64UgyAklD+Kj+GIiMgy3CX4mHcZhy/ rhOp8gc9sejex8B7vNvv35hFd9FfOrQ6aDz5Umc+HJsJCBe3xFzeIvZpszHbeT/s5Ja2 k8hi30LMY5+rMgLoz3fAFN1Kpe0Kow+tG9KSX6ZE3vPJp3QnrvPo5e5RnAXiTZvZZOQI RUzbGD1MrOfyZDUysXI9o6am73OVOmEpogtxOaK03yARrFiN+JnT4ByLwUgxXL/u+7Qt 49XeHzuGw+W8wvb8MJC85KwjnRYuz2Q3B0xsptmojrw/0wCxkreTN3pO9Fs8hh1Ajq3b qZLg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=BKTKcIx1; spf=neutral (google.com: 2607:f8b0:400d:c0d::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.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 g186si37858ywc.29.2017.10.05.22.41.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 05 Oct 2017 22:41:28 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::230 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=BKTKcIx1; spf=neutral (google.com: 2607:f8b0:400d:c0d::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x230.google.com with SMTP id 6so20413018qtw.3 for ; Thu, 05 Oct 2017 22:41:28 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=Q1kV/u3Oz3HZd4IzQ22WH62pmEoJGkXf2Mzta0ykW4A=; b=BKTKcIx1qwFGo7pTgJ1CL8IlVfMt+QGV3r4cNMB7HPAF9YoGa7RUEzszYa9m4T/h0i cAJu7Fmyu4PGAZ1+HKqHYOobfgwvcP7SOL2BX1/StjguBbGh1u4mUvPOhTuGxeZLMSLD 2yGclzdX/IyPSEDFX1icsrPVGFZ5WBcEH2hp7lNaviE347cAWt61zmbQvzv9RMWNcvEd dxu8NYyZPq/Sa8uiDZcKXkRUhW+8cwyam1aQciW7MzdWB7Cyv0z/62WJiHDbMXC0geS1 jGi9LF89tU/iJYWwCN9H1sTNrz2aINi2Di8y8funu6jbt20LXjNcXJt5Q3SFPEe1D9cy PH+g== X-Gm-Message-State: AMCzsaXx1YYUAsVLMv0tMFqpJ99xUm3ukpG953BBRWC+nfNlAWrsw83G i6ckVfMjTWS7I97+goWlEc50sXWH X-Received: by 10.129.152.142 with SMTP id p136mr770010ywg.165.1507268488168; Thu, 05 Oct 2017 22:41:28 -0700 (PDT) Return-Path: Received: from mail-oi0-f46.google.com (mail-oi0-f46.google.com. [209.85.218.46]) by smtp.gmail.com with ESMTPSA id 204sm322664ywh.4.2017.10.05.22.41.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 05 Oct 2017 22:41:27 -0700 (PDT) Received: by mail-oi0-f46.google.com with SMTP id m198so15649055oig.5 for ; Thu, 05 Oct 2017 22:41:27 -0700 (PDT) X-Received: by 10.202.166.9 with SMTP id p9mr483036oie.220.1507268487471; Thu, 05 Oct 2017 22:41:27 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Thu, 5 Oct 2017 22:41:06 -0700 (PDT) In-Reply-To: <27f9b271-c2cc-4a5b-9301-2778be2cfd44@googlegroups.com> References: <27f9b271-c2cc-4a5b-9301-2778be2cfd44@googlegroups.com> From: Michael Shulman Date: Thu, 5 Oct 2017 22:41:06 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Vladimir Voevodsky To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" I met Voevodsky in 2010, when I was a postdoc at the University of Chicago, and Steve Awodey invited me to CMU to hear Voevodsky talk about his work on h-levels and univalence. At the time I was still struggling to wrap my head around type theory. Voevodsky showed us his Coq development, which ended with the construction of a function assigning to each finite set its cardinality, and showing that Coq could evaluate this function on the proof that finite sets are closed under coproducts to compute something like 2+2=4. Coming from homotopy theory and higher category theory, I found it very natural to identify propositions with (-1)-types, and of course every finite set should have a cardinality! Finally, type theory started to make sense to me. This was the genius of his definitions of h-level and univalence, which like many transformative innovations seem inevitable in hindsight: they were the foundation stones of a real bridge between type theory and higher category theory.