From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.194.104.230 with SMTP id gh6mr195226wjb.7.1474575524885; Thu, 22 Sep 2016 13:18:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.218.14 with SMTP id r14ls402297lfg.36.gmail; Thu, 22 Sep 2016 13:18:43 -0700 (PDT) X-Received: by 10.46.5.196 with SMTP id 187mr167464ljf.13.1474575523918; Thu, 22 Sep 2016 13:18:43 -0700 (PDT) Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id w16si7241wmd.0.2016.09.22.13.18.43 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 22 Sep 2016 13:18:43 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.54] (helo=mailer3) by sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1bnASB-0007oo-NI; Thu, 22 Sep 2016 21:18:43 +0100 Received: from client-8-45.eduroam.oxuni.org.uk ([192.76.8.45] helo=[10.21.214.224]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1bnASB-0007YS-DQ using interface auth-smtp.bham.ac.uk; Thu, 22 Sep 2016 21:18:43 +0100 Subject: Re: [HoTT] new slides To: Vladimir Voevodsky , Univalent Mathematics , Homotopy Type Theory References: <6E32CAD6-D1D3-4B4D-973A-BA872F84037B@ias.edu> From: Martin Escardo Message-ID: <42127ebd-c43b-c039-c05e-4f93090527f8@googlemail.com> Date: Thu, 22 Sep 2016 21:18:42 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 MIME-Version: 1.0 In-Reply-To: <6E32CAD6-D1D3-4B4D-973A-BA872F84037B@ias.edu> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) On 22/09/16 20:46, Vladimir Voevodsky wrote: > I have uploaded to me homepage the slides of my lecture at HLF 2016 with a discussion of the Univalent Foundations and some discussion of the UniMath library. See https://www.math.ias.edu/vladimir/Lectures . I like the recognition of the usefulness, and, more importantly, the intrinsic interest in the constructive aspect, given in your presentation. Like you, I am impressed by the work in Cubical Type Theory to make this to successfully work in univalent extensions of constructive type theories. In my view, an important part of the intimate connection of intuition with rigorous mathematics (your slide 3) is precisely constructivity. Perhaps not everybody wants to be constructive all the time, but we do need a good, precise mathematical language that supports constructivity directly, without ruling out non-constructive arguments (by seeing them as arguments that just give much less information one would like to, which potentially one would like to uncover with further refinement). The Cubical-Type-Theory rendering of UF is such a language. Best, Martin