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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-il1-x13a.google.com (mail-il1-x13a.google.com [IPv6:2607:f8b0:4864:20::13a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ad33e6b3 for ; Tue, 26 Nov 2019 00:25:38 +0000 (UTC) Received: by mail-il1-x13a.google.com with SMTP id l63sf15064495ili.17 for ; Mon, 25 Nov 2019 16:25:38 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574727936; cv=pass; d=google.com; s=arc-20160816; b=HWff2xtRkS5DR9Y8myMIaLKtdUtxZ2KNDKXy3cNy3hEXt/34PVMxONsCdiVQTn2Zwq CsFeGCpWEYe4HDvcWJaq8fMt+UoFmcuyuHgmnsPykPn65qzN2Tqiv37bRq+7l/XWI88d No53WuuL1pywEvSvrJOeREKlMX5zKic+Y3jyi605752Xat597YYfpyKe6snjnOSqYw7i KENmU/TWlqLDl3W9y94JEf1xRnfrbNxNcZbmXW8wYZsWR1vdPchbx8Lv3HKZ8S9SNv7z D30pZa7hz1M4fpAdMhxlcfFN70hm7kLaHNvMsNEGb6wjOpRee6y05LCgdb+ubQjYtBO5 FTOg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=O4nbOnHlppjy9Y9f+yIrQ/Hd8O3kKmE8/MAS4Ha4qQc=; b=Lra/0roLArufr1mCAvJsgSOwQ95KiHJddQ7NqkGWAcN4fOI9yeW3JftTgDhtJXmTmy +kDN5z3wckBMSfVV5J6KrhpC56Pwsx4hn8jS4bUo4GPsqAeAEIa1ha3BUQvK6XHUUCs2 2eGh+rcMgAfjNiMT7CSoOtgOiB9vcK2U3erl/SeAGAC7XQUXlEMFQv3MOMb6KNY2RGUh fGWdQcbXXSbMsHzpD2fhJAY44/P1XTGjo6RTcG3oejafAnLtIGb/p/q3UA80iPRDIPvF qbFIYOW1lFmvxYsN8NEJbcgbYqOcOSxwRx9aeYp1bG2aNKilKyz1L/0U0VPmPaa4QVvx ISDg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=QxHQXhEo; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::334 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=O4nbOnHlppjy9Y9f+yIrQ/Hd8O3kKmE8/MAS4Ha4qQc=; b=IBfBwQwS2Ob0upl5gwFr+n3Vpvj91fP4ItnEOttXI34LYuqU8RXgO5AeFsc4k6Ggff FXIYNGmbe5/aZHn4D+3rtWmrQIQJN4HZPnx9FTmNZSrVZjkL2Bdzmsd8T+tMahl30XB5 /ebY7+hOW3MHzhznHjUG4zvejsJWH07KlEGLLYh2bbmfhG04zO8v1Hme1E1oiVxSG/QJ Ktid8p1ydyptufKTxAwLms8xm41sT0egeoLRfFK+oZA3AE4ltU2dPgMTw46JgPZzzsR6 RXn5t5M6ZAI+OtwyBTyacnc5iU2/UGyxSlf01jc/XO5U2uTGRzk3cOjycW0lK+zn3apK TxVQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=O4nbOnHlppjy9Y9f+yIrQ/Hd8O3kKmE8/MAS4Ha4qQc=; b=mILXVxLrpFdfDtReBXz7B8AlvHgY8AT5tedN4WyTRpDC5t0KoRa/JNu7ZcIbHee0Ee cHro21XqENnJnw9Rn/lP++6x+4szzeoZZlcDf7mTvR0WoGATKGGb6ImMZBv7KrsuMSEg mhEIzjOY7OV9NO/XudBgoYwp3me9rYWLdGfOaSTblYwxsXxM1ZfMfCqOXDusptgQFXGT 9i/w8CvYWvOnDAp6QeXmJnsCj6PGQuiY+mUCnApYT2YtXr1P8onGcEvjRZsJOCFG73ek lQWaJs9FgDqmCqwo4Y7RVxKn0DrbhNQhb6K/Ag+HyDIZnhz8Iv875JEkXWW3hoLhHqOS EOUA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUQIlfeBHD7PNsDJEulMFJKiPRGTq4A6sx3WOQY+UAlCSw0hOv7 //cbJESB3QxBMndszGVstCw= X-Google-Smtp-Source: APXvYqwR1d2OWQU77Uwz3zy2vrwe40bI8c8lo0KkGiOsRKpqKxyYlMnsRPreBQL+ju2SLyKr+lAp9g== X-Received: by 2002:a5e:8516:: with SMTP id i22mr19483764ioj.130.1574727936665; Mon, 25 Nov 2019 16:25:36 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a02:228d:: with SMTP id o135ls1351862jao.10.gmail; Mon, 25 Nov 2019 16:25:36 -0800 (PST) X-Received: by 2002:a02:6984:: with SMTP id e126mr13490458jac.134.1574727936211; Mon, 25 Nov 2019 16:25:36 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574727936; cv=none; d=google.com; s=arc-20160816; b=U4fODtlYHsgb4or1jIprA2Yt6jmIDRPQBnuEWo634vUSpJ7ecVbgiEi+9cdG4alb49 7wTy36HDT2Hns8cluv3YHiLvYeAoT/g7GU4dHixJ8ockvnlTc1fgJuJDa0dyMJHvdUXY 4vOXlbbPa8diT/5H0msZD8IFD7GevHt/q/EhOqJ55Bs7hRDjgwRwYRxr/cr7mL96cOvx 3liad65XkYmjmEu47Du3T75tBqc0uoSR/dFtCISG09zzX2k6KH+46hVoKuDNInMWSl8H m0G8OpCyDSQOfg+UyzcEHxyDM6c84ryAEAm8fHBUDT5yAvvg9fvOaVbIcCwlSYLdMHrD S3HQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=+zXQcjLeD7rj8JdnxKdv0MFO78Gmyb3fO9r/Dq77/zc=; b=XQU6whSkf+G85XpU0CEo7Svx6PdKYgJnEAegNyAbTwzwQoRv+qF5Uigbl65p5Si8BM JD3sH9W+CTzHWeHDpx/pJSvCKexB8AVggXYARtOat5UWEOP2FbjCQ+j3XzBkb3CCcFAE IF2ffDJjbMcrAbSyBDc4lVmSp1wqONK7rebS20T06rGhiMyuBRxbO38nM87b5ZU01ky+ 8qS5rZnMSqCrA67aj6Yn0SG+oOqGX7GKqO37NV2qQlp+bGvLLcIZIaiFOxWi8/5eYhIl oSXXxR1j/0/L7ld/qU1FO/jA6HI5YNQmbL4enUpr8SE6I1iTbmuSxdEmHfbRP6tlTh2J 8lgg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=QxHQXhEo; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::334 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-ot1-x334.google.com (mail-ot1-x334.google.com. [2607:f8b0:4864:20::334]) by gmr-mx.google.com with ESMTPS id g10si114759ilb.2.2019.11.25.16.25.36 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 25 Nov 2019 16:25:36 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::334 as permitted sender) client-ip=2607:f8b0:4864:20::334; Received: by mail-ot1-x334.google.com with SMTP id n23so14310055otr.13 for ; Mon, 25 Nov 2019 16:25:36 -0800 (PST) X-Received: by 2002:a05:6830:1e8f:: with SMTP id n15mr380560otr.156.1574727935568; Mon, 25 Nov 2019 16:25:35 -0800 (PST) Received: from mail-ot1-f41.google.com (mail-ot1-f41.google.com. [209.85.210.41]) by smtp.gmail.com with ESMTPSA id 62sm3013277ota.4.2019.11.25.16.25.34 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 25 Nov 2019 16:25:34 -0800 (PST) Received: by mail-ot1-f41.google.com with SMTP id q23so8521202otn.0 for ; Mon, 25 Nov 2019 16:25:34 -0800 (PST) X-Received: by 2002:a9d:7a4a:: with SMTP id z10mr348143otm.283.1574727933978; Mon, 25 Nov 2019 16:25:33 -0800 (PST) MIME-Version: 1.0 References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Mon, 25 Nov 2019 16:25:22 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? To: Kevin Buzzard Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=QxHQXhEo; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::334 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , Thanks for sharing the details, Kevin! On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard wrote: > In HoTT one might naively say that these problems would not arise because isomorphic things are equal. This thought is indeed too naive, but, I think, not for the reason you give. In a non-univalent type theory, you have to prove manually that everything in sight respects isomorphisms. This is I think the point you were making about why the original approach got so messy. HoTT does solve this problem: because isomorphisms can be made into equalities, everything automatically respects isomorphisms. The problem is that in traditional "Book" HoTT, when you make an isomorphism into an equality, the original isomorphism is only remembered "up to homotopy", and then when you apply the transport across that equality (i.e. you use the fact that everything automatically respects it), it takes work to prove that what you get out in fact coincides with what you thought it was supposed to be (i.e. the result of actually applying the isomorphism you started by defining). In fact, dealing with these "univalence-redexes" is so painful that when formalizing mathematics in Book HoTT we (at least, in the HoTT/Coq library) generally avoid making isomorphisms into equalities as much as possible! The only place you might get some mileage is when, as Valery pointed out, what you're transporting is the mere truth of a proposition and so it doesn't matter what the "result" of the transport is. So while it might be interesting to try to formalize schemes in Book HoTT, I wouldn't expect much improvement, and it's not a project I would wish on anyone. What I do think would be worth doing and comparing would be to formalize schemes in some kind of cubical type theory. In that case, univalence actually computes and so you can hope that the proof assistant can actually recover the original isomorphism for you automatically. This may not be quite true (https://groups.google.com/d/topic/homotopytypetheory/wCU0V8RD1LQ/discussion) but it's much closer to true, and I think it would be extremely interesting to formalize schemes in a cubical type theory and compare to your developments. In a nutshell, one could say that the composition algorithms of cubical type theory are a generic implementation of the fact that everything definable in type theory respects isomorphisms, so that essentially all of the nasty lemmas should be proven for you already -- with, moreover, the proofs that you would have given, rather than (as in Book HoTT) a proof that isn't very useful because it takes a lot of effort to extract the "correct" proof. > However my *current* opinion is that it is not as easy as this, because I believe that the correct "axiom" is that "canonically" isomorphic objects are equal and that the HoTT axiom is too strong. This doesn't really make sense to me; I can't figure out what you mean by "too strong". It's certainly not inconsistent, since we have semantic models; in particular, schemes defined in HoTT would specialize in the simplicial set model to the classical notion of scheme. And I can't imagine any way that the presence of univalence could "get in the way" or "backfire". Usually when people say that univalence sounds "wrong", it's because they're thinking of "equality" as a substitutive mere property and "isomorphic types as equal" as somehow collapsing to a categorical skeleton, which is of course a misconception -- HoTT instead expands the notion of "equality" to essentially mean "isomorphism" and requires transporting along it as a nontrivial action. I doubt that that's what you have in mind, but maybe you could explain what you do mean? > By "mathematicians" here I really mean my ugly phrase "proper mathematicians", i.e. people doing algebra/number theory/geometry/topology etc, people who have absolutely no idea what a type is and would even struggle to list the axioms of set theory. It would be nice if there were a phrase for this that didn't sound insulting to us "improper" mathematicians. Mac Lane's similar phrase "working mathematician" is not really any more flattering to the "non-working" mathematicians. (-: Mike -- 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/CAOvivQz3jn5jcjbeeK%2BG2dJ_n_AuZT43pSQ%2Bq5z8Roq_YFzQpw%40mail.gmail.com.