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.8 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 eab71213 for ; Tue, 26 Nov 2019 08:08:53 +0000 (UTC) Received: by mail-ot1-x33c.google.com with SMTP id m14sf199670otf.3 for ; Tue, 26 Nov 2019 00:08:53 -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=stz76hYB2dfcDZHIbadNEBZWKmsKN7/dy6ttXqOxnE0=; b=ApjmAWmKF8trq+HVl3Poh4StH+p8S/SvAB+79ZnaAeveoJMUZJ9hbC63hw32paR0el s8KDmJenWBqQjA++nl/QopT+PGK1G+p6VyeN6cdXqf2rxYDorrqgzhzHuHZOVCBxW88l 1oTGDMymN/nVjYIf2X7KydLAuaeyFdl2xWKUlASbfpvBZKyqpNTIVdbRJxaqZ7UVb6X6 ST0eH7o2KxprXgTy5nNtS2VdSow0iqU42QlCyqkFKOMs9EK5UHOBlpmRHDXmcAYGP3Z3 ReaDTGMcctU6eO2jYktroD2NsnLYDtpJUCGnngSkNRq+9OVnN7FeWRwMsINsrGnrEBxn a+ow== 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=stz76hYB2dfcDZHIbadNEBZWKmsKN7/dy6ttXqOxnE0=; b=QSYKUpG9OkvNz7z0YZ610EhLHwKWNDa/FRVYY5b/viAH2cyFUOn4zhSEofCyluV1O2 avSaYs6mWM53/bl8sgiQ/DAtblewvlEhL/QaqlemQoaH0Xi+nvcptvQ8b/gHCMUEiayg w451S4ItB595KLXehhWiIzyIIodEdFnY9QOFnwZLnOIFSZWe475rpDEyR3aIA0FfBp2Q bL119BS9TP1SgUta2pjohARmymGageC/o8mmuSq9yDAQK5ZXoKYsEb3VcVbp+x3NbjAv kCedgdhMiXkhoZINFJcSQjQM2trNzDn/xoB4uU5JlGE4qxx3zeHZY7fk5PQe3ROuCDHN tTXA== 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=stz76hYB2dfcDZHIbadNEBZWKmsKN7/dy6ttXqOxnE0=; b=gb3Zog+ufFslrHeWh+V2ePuNG+HVYhKNAMsgrJzRDADUW6eY6bv1jMqAASBae2NTEc u4NZrPVjT83K14A4NiTx6IMhbP8/zyEBqeMS/rba/VDxTyBm3DM8Rx3pGYS/YjW1XGZr lD1HvN4aLLX9iALDoJ+j0aaYj0Ngo+A2hFP4QOeEwurjQs/QREXpR7azrY76gWujBye8 2WfgyZD1jVGp55VDQsMDYSl9LM+1Objr8jITsJIz9kjjP57JJykrePNZS6fHqoolqWBN cKVFVZNTh7UaKFKZA82/iahloV0gOi1cs2aESteMHNu8m+zEwJAvnBWViGwKnlWLFaE3 5xZw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXSOg0yIs6vJu1TVYdfGgAI4Kzp1yUo6ph55s8WAoICdfJ4KcvC N+A/Tlre4Eb+MKv7qJKqpIs= X-Google-Smtp-Source: APXvYqzEWyFGAPh+3XFCGt3F+aJ6bN4rlT1fZ1xyWqkgZ+IDQO+GzZEj3z9IE6AdDkaeqBg9IE9Nkw== X-Received: by 2002:a9d:1b4b:: with SMTP id l69mr1390128otl.303.1574755732419; Tue, 26 Nov 2019 00:08:52 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:2815:: with SMTP id 21ls2665935oix.14.gmail; Tue, 26 Nov 2019 00:08:52 -0800 (PST) X-Received: by 2002:a54:400d:: with SMTP id x13mr2394185oie.119.1574755731716; Tue, 26 Nov 2019 00:08:51 -0800 (PST) Date: Tue, 26 Nov 2019 00:08:50 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <2f61877b-b4ef-405a-99cc-85da227c70bc@googlegroups.com> In-Reply-To: References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1576_501194479.1574755731115" X-Original-Sender: UlrikBuchholtz@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_1576_501194479.1574755731115 Content-Type: multipart/alternative; boundary="----=_Part_1577_429849439.1574755731115" ------=_Part_1577_429849439.1574755731115 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Tuesday, November 26, 2019 at 1:25:37 AM UTC+1, Michael Shulman wrote: > > On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard=20 > > However my *current* opinion is that it is not as easy as this, because= =20 > I believe that the correct "axiom" is that "canonically" isomorphic objec= ts=20 > are equal and that the HoTT axiom is too strong.=20 > > This doesn't really make sense to me; I can't figure out what you mean=20 > by "too strong". > Of course I agree with Mike that univalence is not =E2=80=9Ctoo strong=E2= =80=9D: it merely=20 implements the mathematically right notion of identity for types and other= =20 structures built from types, such as rings, etc. But if I may venture a guess, I'd say that Kevin wants a =E2=80=9Ccanonical= =20 reflection rule=E2=80=9D: canonical identifications should correspond to ju= dgmental=20 equalities. We've had some discussions before about the underlying meaning= =20 of judgmental equality (invoking Frege's Sinn/Bedeutung distinction among= =20 other ideas), but I don't know whether we tried saying=20 judgmental/definitional equality should include canonical equality,=20 whatever that is. This might be really useful, but I think we're still some ways off before= =20 we can implement this idea. The first question is whether =E2=80=9Call diag= rams of=20 canonical identifications commute=E2=80=9D. (Besides the obvious question o= f=20 defining canonical identifications in the first place :-) But the adventurous can start by playing around by adding canonical=20 identities as rewriting rules in Agda: see Jesper Cockx' recent blog post:= =20 https://jesper.sikanda.be/posts/hack-your-type-theory.html Ulrik --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/2f61877b-b4ef-405a-99cc-85da227c70bc%40googlegroups.com. ------=_Part_1577_429849439.1574755731115 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Tuesday, November 26, 2019 at 1:25:37 AM UTC+1, Michael= Shulman wrote:
On Sun, Nov 24,= 2019 at 10:11 AM Kevin Buzzard
> However my *current* opinion is that it is not as easy as this, be= cause I believe that the correct "axiom" is that "canonicall= y" 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 y= ou mean
by "too strong".

Of cours= e I agree with Mike that univalence is not =E2=80=9Ctoo strong=E2=80=9D: it= merely implements the mathematically right notion of identity for types an= d other structures built from types, such as rings, etc.

But if I may venture a guess, I'd say that Kevin wants a =E2=80= =9Ccanonical reflection rule=E2=80=9D: canonical identifications should cor= respond to judgmental equalities. We've had some discussions before abo= ut the underlying meaning of judgmental equality (invoking Frege's Sinn= /Bedeutung distinction among other ideas), but I don't know whether we = tried saying judgmental/definitional equality should include canonical equa= lity, whatever that is.

This might be really usefu= l, but I think we're still some ways off before we can implement this i= dea. The first question is whether =E2=80=9Call diagrams of canonical ident= ifications commute=E2=80=9D. (Besides the obvious question of defining cano= nical identifications in the first place :-)

But t= he adventurous can start by playing around by adding canonical identities a= s rewriting rules in Agda: see Jesper Cockx' recent blog post:=C2=A0https:/= /jesper.sikanda.be/posts/hack-your-type-theory.html

Ulrik

--
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/2f61877b-b4ef-405a-99cc-85da227c70bc%40googleg= roups.com.
------=_Part_1577_429849439.1574755731115-- ------=_Part_1576_501194479.1574755731115--