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-pf1-x43e.google.com (mail-pf1-x43e.google.com [IPv6:2607:f8b0:4864:20::43e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3427e8dd for ; Wed, 27 Nov 2019 08:22:53 +0000 (UTC) Received: by mail-pf1-x43e.google.com with SMTP id b17sf13606208pfb.8 for ; Wed, 27 Nov 2019 00:22:52 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574842971; cv=pass; d=google.com; s=arc-20160816; b=HsUKQpB0XWfO22AodVnhMm4/9HZ/oDoxBWK4SmhfpzI+Hlv4tRi8OaHUgDASQ4+JcR V0CavQDkOEu4JOsys/aosFpX8CSzlhejd6QriUIvm7pzTUCbSNTY7WrECP4xuxOA1R9B w2HJAZXLhgtbVUsVaahp5W2emW4Z6T8j4ZySjZvGtAvyW0UiwboRaCjthMVSudKJRmN/ +bc0UzqoYKgKOW0dkXeghl3abkbwVsFCNSLqw5zFU2RC0xpGmOFv4PbeXZvj5KrgV9BQ q7GUEblRh1mtMSC7947MPmfnZTM26hwaWNS33vBpw0b9IyxEVMmsBaJ+2V8gUzUTtjCh mr5Q== 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:mime-version:message-id:date:reply-to :user-agent:references:in-reply-to:subject:to:from:sender :dkim-signature; bh=y/Akg6vzIZP5Psj5MxTl6CsnJmALMVRofjXWJg1mi34=; b=meQevlWIfseEVIPHwsWBprEugGski7yWkGImfqBmnGYKMgDq+0RUPIRME8Ab83bWBx bEIcf/01qqqnQCe6hWTpiyuH1uJEglI+/YYReoh6wt3YmAtefI8kAWj+jRfmWMxtdQMr J21eumSx9y4PuNn6w1KTF5kY+1uZLfwefupwSi8PipAEoJMGfO3p03WOyaGcDa1QQL1F jrNvq4MlQCatpu/PG4dWG39B+RC2Scp5b4fZEjdPTwYmIU/LEEPaZ+lg1+PTL+JUkZ9i +HQDItBGgcYwdBcvQYB5eomTYMoOt4zWbXUSUoDhaiVtGj0JbeanKakcQBSqm9e1W0Es y3Lw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of raghu@retrotexts.net designates 23.83.212.4 as permitted sender) smtp.mailfrom=raghu@retrotexts.net DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:in-reply-to:references:user-agent:reply-to :date:message-id:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=y/Akg6vzIZP5Psj5MxTl6CsnJmALMVRofjXWJg1mi34=; b=jnSbqYN/y8eOmtnODtVbtfQVncZMigBDzjnGkcKBaer2e56mj5kmAt0skgv6hAFqcr RnfXX/TDxFwraAXAQ6hKy3KEdndPopFgeFf12bAvnuFT08n/48Bel4RYPdAc6CyEkQ// Tte62tWYxf7wJbzbZzt/pJJVSKspSXTbCpNIK9X0+0VZF13ucIUlzY/S+mFFdVM+rXQA XLJVpGxIdSnEadnHiQ2Rsrp+4v6H5tNWSomYtnSu6QEc/5TFGzq//OxJoe3yD3wHkn0F +gBNoLN84WG8nwwvEmhJvJ8Rc9n6RleV5ciWotP+rbeJFf0oRcwJAOWTvb6OMxlw1J95 Dujw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:in-reply-to:references :user-agent:reply-to:date:message-id:mime-version: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=y/Akg6vzIZP5Psj5MxTl6CsnJmALMVRofjXWJg1mi34=; b=COPiF76pJVEeznELVmkiL4l6FLiPi3+mODG2CNw3pmeF43rjbgtUjqS7beSlsgeNPK 7lUU4laNtBeo2jNLLLofQGpsFkIZS97lbUkPSs6CDPOcC2UVMPt+O2DiCifhFCTa16fj 6Uj+M/UXMD2zSuzt4g/V+/BBQWwqf87V4F0f53SrSgnNX1M+qXTOhwCuSifO+0pafagD VapOeFOhl0Vl5hKYZ3VQYgECnOENrvK7QPkWJ3JK6bSQfI3NH8/myUITokmg3Ls5jviv HP1VCZfocXSqzP299ZrxaDAGNC90oLPzYMREgJ1k3acjBMErQciscrPns5Ly3wrLsb/B 85sA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX5j/oNXar6NWrt/RZWXd124oNi8JAzi2hRvo+Qo4Rw9syo2irt I1qprO9Ltm7ggQwqSznY/MU= X-Google-Smtp-Source: APXvYqyvTnxhjq6XsAWoGWyvg0rV7y/NrO1/oXM0tQU2qIPCtG9XGcvv0fIFNaykJb9i2L77Qg5gHA== X-Received: by 2002:a17:90a:b28c:: with SMTP id c12mr4374753pjr.22.1574842971652; Wed, 27 Nov 2019 00:22:51 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:567:: with SMTP id 94ls576113plf.8.gmail; Wed, 27 Nov 2019 00:22:50 -0800 (PST) X-Received: by 2002:a17:90a:a405:: with SMTP id y5mr4562924pjp.102.1574842970729; Wed, 27 Nov 2019 00:22:50 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574842970; cv=none; d=google.com; s=arc-20160816; b=IhLUUf1wIO0hyNfUdsLVO3wYhVSXwHIukxFZILJSl/GoKC0/8fwAlqkk2VyAqxkLCr tqJOl9b8k/u4eziiULppTQtQyiWhABRLF6eVW0Kav6BmBT3paxaJjBgZVCG0MCaXEBFE 23G2O/2cG0ZmouTWYOkwG7qcBytj0E4oybTLJaWa0G94h3SwlsTG0ARTTfq9BvAJyrZr ddHpLzRyVvEB0qBTxXaRpLgBLkomg7MLmjUjRiOziSGfFhqHLNSMHvlaIrIkDh2mm9f6 81Vx4bAx/8ohfPsrQ0j41XG4nOwsFtA3rXNZ7oVDm1u9Eyb1ngEyLpptUO2JrXklKo8Z qatQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:message-id:date:reply-to:user-agent:references :in-reply-to:subject:to:from; bh=bhYO+ccgEkh/UWX8ilyd+6oh2k5+tjp4iWBjogBcPnE=; b=QWd+Ppw/Nwte8SR5r9yfwWwRuaOa0I52bufBYyZisSGEvt5AKunorYiTerXJcQhAMa H3XoYE/PtzfaRWDvGVut9ed2YVFHWyEVx3LxfNlO0tUFvFFFq+EWpWzqkqBzzH8iwPar b/3HaA/cqcoHx+huw+LQqNXFXB62YMiJTlCG5SO3DVSZJMHR6VUG/rfSr1SEQhdnIeWe gTkZlmv5i76cu+D8arj3q0KAKPzzHY4U26B+qzUtwUq3riFfFBzjINSN37/MwTWp1LvP +ivzvpmvUHBSiZV4Z8ym0Uvs6GKI5LiztYdPaHHhGOCapOIOQlmWD6jm2IUaqdHNS7dG UAlg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of raghu@retrotexts.net designates 23.83.212.4 as permitted sender) smtp.mailfrom=raghu@retrotexts.net Received: from antelope.elm.relay.mailchannels.net (antelope.elm.relay.mailchannels.net. [23.83.212.4]) by gmr-mx.google.com with ESMTPS id j19si606073pff.4.2019.11.27.00.22.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 27 Nov 2019 00:22:50 -0800 (PST) Received-SPF: pass (google.com: domain of raghu@retrotexts.net designates 23.83.212.4 as permitted sender) client-ip=23.83.212.4; X-Sender-Id: dreamhost|x-authsender|raghu@retrotexts.net Received: from relay.mailchannels.net (localhost [127.0.0.1]) by relay.mailchannels.net (Postfix) with ESMTP id EE7F36007AB for ; Wed, 27 Nov 2019 08:22:49 +0000 (UTC) Received: from pdx1-sub0-mail-a45.g.dreamhost.com (100-96-14-7.trex.outbound.svc.cluster.local [100.96.14.7]) (Authenticated sender: dreamhost) by relay.mailchannels.net (Postfix) with ESMTPA id 3F2036004A3 for ; Wed, 27 Nov 2019 08:22:49 +0000 (UTC) X-Sender-Id: dreamhost|x-authsender|raghu@retrotexts.net Received: from pdx1-sub0-mail-a45.g.dreamhost.com ([TEMPUNAVAIL]. [64.90.62.162]) (using TLSv1.2 with cipher DHE-RSA-AES256-GCM-SHA384) by 0.0.0.0:2500 (trex/5.18.5); Wed, 27 Nov 2019 08:22:49 +0000 X-MC-Relay: Neutral X-MailChannels-SenderId: dreamhost|x-authsender|raghu@retrotexts.net X-MailChannels-Auth-Id: dreamhost X-Tangy-Macabre: 6b49d421779d3158_1574842969668_1431754696 X-MC-Loop-Signature: 1574842969668:2966999051 X-MC-Ingress-Time: 1574842969667 Received: from pdx1-sub0-mail-a45.g.dreamhost.com (localhost [127.0.0.1]) by pdx1-sub0-mail-a45.g.dreamhost.com (Postfix) with ESMTP id C9B25A5D49 for ; Wed, 27 Nov 2019 00:22:43 -0800 (PST) Received: from retrotexts.net (unknown [14.139.59.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) (Authenticated sender: raghu@retrotexts.net) by pdx1-sub0-mail-a45.g.dreamhost.com (Postfix) with ESMTPSA id 5B1D3A5998 for ; Wed, 27 Nov 2019 00:22:43 -0800 (PST) Received: by retrotexts.net (Postfix, from userid 1000) id 736422400340; Wed, 27 Nov 2019 13:52:38 +0530 (IST) X-DH-BACKEND: pdx1-sub0-mail-a45 From: "N. Raghavendra" To: Homotopy Type Theory Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? In-Reply-To: (Michael Shulman's message of "Tue, 26 Nov 2019 14:18:34 -0800") References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.0.50 (gnu/linux) Reply-To: "N. Raghavendra" Date: Wed, 27 Nov 2019 13:52:38 +0530 Message-ID: <87k17lafu9.fsf@hri.res.in> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" X-Original-Sender: raghu@hri.res.in X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of raghu@retrotexts.net designates 23.83.212.4 as permitted sender) smtp.mailfrom=raghu@retrotexts.net 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: , At 2019-11-26T14:18:34-08:00, Michael Shulman wrote: > Personally, I'm doubtful that one can ascribe any precise meaning to > "canonical isomorphism", and therefore doubtful that one will be able > to implement a computer proof assistant that can distinguish a > "canonical isomorphism" from an arbitrary one. I have usually assumed that canonical isomorphism meant functorial isomorphism, i.e., an isomorphism between an appropriate pair of functors (which are generally left unspecified). As has been mentioned, there is no functorial isomorphism from an arbitrary finite-dimensional vector space V to its dual, whereas the usual isomorphism from V to double dual is functorial, so the former is non-canonical, and the latter canonical. Another explanation I've often come across is that a canonical object is independent of the choices (if any) that were made in its definition. I guess the notion of independence depends on the context. Raghu. -- N. Raghavendra , http://www.retrotexts.net/ Harish-Chandra Research Institute, http://www.hri.res.in/ -- 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/87k17lafu9.fsf%40hri.res.in.