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.9 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-ot1-x33c.google.com (mail-ot1-x33c.google.com [IPv6:2607:f8b0:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 745c194a for ; Tue, 5 Nov 2019 23:14:10 +0000 (UTC) Received: by mail-ot1-x33c.google.com with SMTP id v13sf2897292otf.13 for ; Tue, 05 Nov 2019 15:14:10 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=EkFYI3CVW1x+fEViJYFeerH4Qlm7H0i6SvIqJX2kN/M=; b=sDJaD1bNq72a1EUEBzZjYVnMhGEm6Vcs8zXyd4FoDfGdl/xNe06WmwlF/p5Lui5e67 uQsTFziekZfbCi+CAhmcGPRn4VdiqZGqGHmwdGzOo1lfW7dNIk/R6+sS9iITvrdMV/w1 cZYOK++XibBbR/Cnx2JDyA2tv1HmaJ1JEBuWvIUWP6Nt4qxc8ADtUr2iIygLIIZWcnyA pLMyikAkS3hB4m+e1nlyMx+v/K70wZt6rK2qHVGgRnZN2c/UnNi6XrBRSsiKGXojMs/c j2Eu/EyJG1rDzsK5AtldhPKs0/+00M0wadnrHdqbFw6sXbQ+bQGScrB8BPR+Sm5EJDQI JwVA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=EkFYI3CVW1x+fEViJYFeerH4Qlm7H0i6SvIqJX2kN/M=; b=HsZMS0I5ZY6z23bS6JBjlrFm+JqI283pcZhNcKEwX4vykjb326Zj8YmhIZqqX/zkYg gYd2FiunngSrY+IhzzKlnQA2tu7/kQP1qFufkXY2+l6l5Wyn43NcftiEWs2QEel0Iko1 hevq+m8WD7ZKS3g5yEEji90KTs3LHxQXkYKJ789yJg7S46v1dHVJuwgorlHsGZzYYjVs WhOjHr3PiAZbkxnSy7H6h4B08+0D/WIWrx8NVoVi5b48zTAuo/mokWW1aHwGIK6e0Uhe vlvoZ5pEXfWDRy9EFZsE/XhSjtsFaBj00xa5wYdDW8Em8u1XB2APf986Bx1CzxVAkEqV OGfw== 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:in-reply-to :references: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=EkFYI3CVW1x+fEViJYFeerH4Qlm7H0i6SvIqJX2kN/M=; b=UEgvOtpSoXsDl0QzenvdX6M7UXr4AVvygRbf04UhTDXVEaDOhxCcD7xT/+z3D4dDhi btCep/F2PGJeiuoWXyiW0fMJy17Q2jwo7vIG8CDEPn4YM6B5UY7xnW9gryJ5ZiOdx72R GAlOL9NRNRExGcUrVJYYwNWPkjaOVq3NPZgoevS7DX5hmTbpF5eTvaPS3KLVMk2FcQSP yDxOXsy8MKOzMeb8+N66+M649cpEXsFGmhWwRQi9y1SUuedMyxHckxZw3X40jt/Pxai/ cSgB4s9IMfdnCQJv22dSkRFZIgSHLZxNf77Mt1F2SAcj0SmbCbDBa3YBTrRcyH7Ysot6 cBqA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXJ27qmTlvRq7KAoD0Pqq4quRvm9A/SC9x7HZfrOdneDRmUoYim +4SGbULREACegia4BheYBsg= X-Google-Smtp-Source: APXvYqzQdOQW9C9y70XLLRB7SeWa6j1vNr2ib+J1AnZucE7MFzlPWHyDSMCes/EMaINBaCWOgv3VJg== X-Received: by 2002:a9d:191b:: with SMTP id j27mr22958483ota.230.1572995649049; Tue, 05 Nov 2019 15:14:09 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:5717:: with SMTP id l23ls108154oib.1.gmail; Tue, 05 Nov 2019 15:14:08 -0800 (PST) X-Received: by 2002:aca:5955:: with SMTP id n82mr1266383oib.37.1572995648331; Tue, 05 Nov 2019 15:14:08 -0800 (PST) Date: Tue, 5 Nov 2019 15:14:07 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2116_2123141164.1572995647749" X-Original-Sender: escardo.martin@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_2116_2123141164.1572995647749 Content-Type: multipart/alternative; boundary="----=_Part_2117_1057897035.1572995647749" ------=_Part_2117_1057897035.1572995647749 Content-Type: text/plain; charset="UTF-8" On Monday, 4 November 2019 18:43:08 UTC, Kevin Buzzard wrote: > > It is exactly the interaction between constructivism and univalence which > I do not understand well, and I think that a very good way to investigate > it would be to do some highly non-constructive modern mathematics in a > univalent type theory > Regarding *old* mathematics, you have the well-ordering principle proved in UniMath (from the axiom of choice, of course). Regarding your doubt about the interaction, we have that univalence is orthogonal to constructivism. In fact, univalence is not *inherently* constructive. It was hard work to find a constructive interpretation of univalence (which happens to rely on cubical sets as in homotopy theory). In particular (even if I lam fond of constructive mathematics, as you know), I work with univalence axiomatically, as a black box, rather than as a construction, in my (formal and informal) mathematical developments. And I do prefer to work with univalence-as-a-specification rather than univalence-as-a-construction. There is nothing inherently constructive about univalence. There is no a priori interaction between univalence and constructivism. There is only an a posteriori interaction, constructed by some of the constructively minded members of this list. The constructivity of univalence was an open problem for a number of year, and I would say that, even if it is solved via the cubical model, it is far from being fully understood. Best, Martin -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/cb153658-548a-4fe9-91ed-fc2e3db33723%40googlegroups.com. ------=_Part_2117_1057897035.1572995647749 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Monday, 4 November 2019 18:43:08 UTC, Kevin Buz= zard wrote:
<= div dir=3D"ltr">=C2=A0It is exactly the interaction between constructivism = and univalence which I do not understand well, and I think that a very good= way to investigate it would be to do some highly non-constructive modern m= athematics in a univalent type theory

Regarding *old* mathematics, you have the well-ordering principle pr= oved in UniMath (from the axiom of choice, of course).=C2=A0

=
Regarding your doubt about the interaction, we have that univale= nce is orthogonal to constructivism.=C2=A0

In fact= , univalence is not *inherently* constructive. It was hard work to find a c= onstructive interpretation of univalence (which happens to rely on cubical = sets as in homotopy theory). In particular (even if I lam fond of construct= ive mathematics, as you know), I work with univalence axiomatically, as a b= lack box, rather than as a construction, in my (formal and informal) mathem= atical developments. And I do prefer to work with univalence-as-a-specifica= tion rather than univalence-as-a-construction.

The= re is nothing inherently constructive about univalence. There is no a prior= i interaction between univalence and constructivism. There is only an a pos= teriori interaction, constructed by some of the constructively minded membe= rs of this list. The constructivity of univalence was an open problem for a= number of year, and I would say that, even if it is solved via the cubical= model, it is far from being fully understood.=C2=A0

Best,
Martin


--
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/cb153658-548a-4fe9-91ed-fc2e3db33723%40googleg= roups.com.
------=_Part_2117_1057897035.1572995647749-- ------=_Part_2116_2123141164.1572995647749--