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-pl1-x63f.google.com (mail-pl1-x63f.google.com [IPv6:2607:f8b0:4864:20::63f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id fd3bb793 for ; Wed, 27 Nov 2019 16:37:45 +0000 (UTC) Received: by mail-pl1-x63f.google.com with SMTP id h8sf9498480plr.11 for ; Wed, 27 Nov 2019 08:37:45 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574872664; cv=pass; d=google.com; s=arc-20160816; b=uCWcVjoyDge8MjjcqT1vCOSHKqqADGf0WziTVgI3+s9Gkz+JH0zYSiEq8jlGGCV6By fcIBuR+tKn/OcWrTeSUa1Bi481zAt3SsGj7aU03oiK6lTw9WRnJwo+HW9AIrKCYVGPHB T7SktRn5ShkFwC+Fo7tPAXIZ88H9kfnysnzCc8Shg3GoiIcr9mH9OJxIK59lAiz6KtMQ EkZFcGkhlisUUU9QEjcSf4w70MrisxuIgqbVMcNufc6Ezzooc6C6T9O9fBlZux8zMe43 o73dR97o0a3FPoTVuXAludz0BB7drVpBnOJOzb/jZ8lvHMA4UutZ6j4ddik45U0wF3nT yI1A== 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=Yy0io3kDZfR5hMDOuf9l/poFO+H8QHEpfa8wgNSnAxI=; b=HdBpaPdfq54nDF5XrB+tdJAQRy1v6OLYFL5hhsqMx7gVFwk0pCOvK0PjyR3xA+nssH wPfyQiyEx1zZDBeEFt1zlHxqq7QMm/AkIc1ITEAcQqQxBDuchvbqx9Z6q6IwhaqgxNBS fH+wY2sNam5kFHlWbSxKOGkea8B4A0WOZE7L5UdFwkK/23paRqQWtYHJjTq3gGOHlyiL DiDtgH9V+WRkCHq2l+NMH+v7EJAOPQ2Ex40zkIcbtUu4L/KKVSeDUq8Imkmq9AqQEms6 JolFIv7+kuxHyN5cE0EhErcD90Mrxvs1OeDF0+PKPrmzm2OViYpznZKj2hvvhcWp1N5N JclA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=pkGgnExg; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::229 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=Yy0io3kDZfR5hMDOuf9l/poFO+H8QHEpfa8wgNSnAxI=; b=jPCxGeNWGa4bFpquPKgvIgildA/ig/xF7NsGHdEoiX8eGEHUgZjWRXVSUb44OTVwhX 2cCvQ6a1fYO/Q7QGkCnkmXbI12x773zTNv7v5xWzvboGURzTFfPgh4NL5VskLR6NlINh FQhTQXG//vZd29Cv4MB3+NUYmPgJ2/2MD73E0DXZCeQ30fvZ8v2INNW4boPoOBpyVcCC Wypr7QqRaY6JFX0wmjNk9BQ/hN30XViYhiwekeA7+jg/oYjqtSS7hfNwl0G9CEiGorUq 66MAJRMSahOv13/0fXYhtiC6ii00I52JHlurmzzdyajAu2iqRMx8PJs8qp2rCd+enVuT aENQ== 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=Yy0io3kDZfR5hMDOuf9l/poFO+H8QHEpfa8wgNSnAxI=; b=LTR45v4AuCKM4MH/w1Is9+YgPpotlJNtWW7wM3biKqUe9o8yjp25W9gFlHykMEn7zl JbCcOqqLKi8kpIN0Mv1HqPAF3mYfjryU6jmke5aW1qYWYqplWan82eLtAU9FWpq1LdM+ eoBUfYiBZzxE18B0iH1XkF9qLYyiO7CMGAO93zct6zZMPG6i1bS2XtucUNoRXApaEwvF D2GaT0V5pQHsp7wkk595jH4/+YESa7BRcBPYdNn03bck+M+r+QcTHEqbM/8KjcsjhWQP ZMQeZ+7Aq/htBdCr5KOOsukiuixf5vr0aZhaUCNYJQtHUd4RXLlJJYgfIAWjmpa7QX+5 0xzQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWHS82SmQk+HEklsRnti0M3B+bIpDoiMOdeLO9huVCOoE+/LjSH kYs5yJLJdMU0UH0V8z0oo1w= X-Google-Smtp-Source: APXvYqzEpvI7yOhXpw4E5o75SRlzCiinxv4P+SFA+788zrYZWV9o4VdcUW9twa0Qnm8GNNaIzRLmPQ== X-Received: by 2002:a17:90a:19d1:: with SMTP id 17mr7094513pjj.52.1574872664087; Wed, 27 Nov 2019 08:37:44 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:b704:: with SMTP id d4ls3980365pls.16.gmail; Wed, 27 Nov 2019 08:37:43 -0800 (PST) X-Received: by 2002:a17:902:be07:: with SMTP id r7mr4971989pls.33.1574872663230; Wed, 27 Nov 2019 08:37:43 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574872663; cv=none; d=google.com; s=arc-20160816; b=K2EZ7+gfrZaelB9V2bQqkDru55qg63uYBbRQELsv+y7IEUZID+f/6gjsNfrzLvfWdd L2toW7LL77md/cnUSasepAWbscrNJbXpCg3C3okn2CiH4royjR1f0Blk96/h7XTBERic wCSd3oR34ihMTVpo0R6PgdNgYCpKgVCSntVy6Ftyy6tEaIl80Ueer52Ts4gNSLChF6kN i22gdrxnZhcoS2WlUGTGZF8P4xSQQBCXdEzcDj/JwGDuYEy54c5Yzf0MB8onft41/DXG mBQpcAdxvDdJH1Z5dwj6fMoExJPrOeUiRInKcFB98GQZrjJ7B+6LgUGB5i63wXqIALDl 2snA== 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=DVnibpE5zBdbI/blRNqIAFcfGEPHxVjWvr43lEk1aXY=; b=P424mSIi2QePai/N0PtgW0Zvc+WFU+rj65mroJPaas5ZvSWH5Wy2qi3EJCnFku9ePc AqXReNah28L6ZWb6QLlePPHo2DoMR9+40ZdF3Zt/eFhUCOSXE3cT5XRGgmR9VPWMcmpm cTDg0SLf/IAwDgdHylqU43/vECVxRq85pmp2TVtYtMDwtEuOrqxyJED86rkSbDNPoVSY Cl2J6TEaYljtC1BdeR2Vb3iLHt7xMiucoU6AmFBOQPfQwG1yoHgj5e75LLHjk6dYo0PO WDBmskbzucwwYraVnRbmMxdvIfliR2q9N4N5ueGggXU/d4YQX/abV/ewYFfr27vB7+YP sVGw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=pkGgnExg; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::229 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-oi1-x229.google.com (mail-oi1-x229.google.com. [2607:f8b0:4864:20::229]) by gmr-mx.google.com with ESMTPS id m11si221722pjb.0.2019.11.27.08.37.43 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 27 Nov 2019 08:37:43 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::229 as permitted sender) client-ip=2607:f8b0:4864:20::229; Received: by mail-oi1-x229.google.com with SMTP id d22so20640773oic.7 for ; Wed, 27 Nov 2019 08:37:43 -0800 (PST) X-Received: by 2002:a54:400d:: with SMTP id x13mr4764912oie.119.1574872662708; Wed, 27 Nov 2019 08:37:42 -0800 (PST) Received: from mail-oi1-f180.google.com (mail-oi1-f180.google.com. [209.85.167.180]) by smtp.gmail.com with ESMTPSA id 9sm5053340oiq.33.2019.11.27.08.37.41 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 27 Nov 2019 08:37:41 -0800 (PST) Received: by mail-oi1-f180.google.com with SMTP id 14so20595510oir.12 for ; Wed, 27 Nov 2019 08:37:41 -0800 (PST) X-Received: by 2002:aca:edd8:: with SMTP id l207mr4692879oih.102.1574872660953; Wed, 27 Nov 2019 08:37:40 -0800 (PST) MIME-Version: 1.0 References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Wed, 27 Nov 2019 08:37:28 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? To: Thorsten Altenkirch Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , 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=pkGgnExg; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::229 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: , I find the wide variety of opinions as to the meaning of "canonical" to be evidence for my contention that the notion is not formalizable. (-: Personally, I feel that the closest semiformal approximation to a "canonical" isomorphism is one that's declared as a coercion. -- 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/CAOvivQzEF4sqoKtaRNVA_wN-vfEDV3UEzE0U1E%2B9i0jbjpHC_Q%40mail.gmail.com.