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-x338.google.com (mail-ot1-x338.google.com [IPv6:2607:f8b0:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f06693b4 for ; Tue, 26 Nov 2019 20:40:51 +0000 (UTC) Received: by mail-ot1-x338.google.com with SMTP id y65sf10711203ota.18 for ; Tue, 26 Nov 2019 12:40:51 -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=CIrgehgcDS8vSeIeCDFEZU5ft8iDj9IU+HW1I7OtsY4=; b=iUejEO3wslqiOqfKnjk5pab99rI66aVi60DZnEo4OSSIRYGsKQyr+oaw4JPQ5VVL6H mepLrAcuNK7aPrOGqQyWqZpPltqRf4ahzmStd+1/ASBI8ZVUlNLHOR9OdoP+cZZri9hJ 7z6DdmqpYqqXJ0yZXhlQnF7qthL96H6XmO94Rr5+LbXgoWLaFiETYX68ossNndHVAxOL XLO02vim3yZ04H5NNNsH1fBJ95WWafgNE4wnpMKrcmfpAVrvKNmHbxjxikDs25OaB0NB 8ixZ3OKMdOqr3con21MAw3Mxra6uSMuMScBhbmxMDs/Z+DyS5Ser54LdQJol79Wb9cO3 vqCw== 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=CIrgehgcDS8vSeIeCDFEZU5ft8iDj9IU+HW1I7OtsY4=; b=luQGRqOau0zTg9ROOV9xfF0HbCeVZfc8ehTvEpZCzv06pnR2VR2EX3k5aH6VX3K4v2 JjVfh4uk+z7zcfWV3DsEO+uulMh/M3WxBNXf6iUPF1JWYQbA0OX5W0jyyfhwgeQu3BtI Dsk01/f0uqMSXgJDoYpsxA3FJFD8EORNyunHAiqNWmPpvy9SU/OXg1q9/WEcZsXjqSN/ VT4+itJ89JtvomrvwUAeOLykbZfYsOMLiOkVzkx81B81NfHnc7uPHgpwgO2XDf6hANwP 3L1CE0SCiwimnba7qqmrbirV1I2dsgtkv32hMLLFJtU2DUhYumng9C2MlMzA/mQtNV9x gFwQ== 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=CIrgehgcDS8vSeIeCDFEZU5ft8iDj9IU+HW1I7OtsY4=; b=mCGGBWRldMn7vOeCCGuWwvDWFL9eCln0YspQxPPxFmBhbNhJFoXPuxCWZXwvLSd5qr wCaM5h2rYaNCcRY0YhTNmMp58XQW2b0j5e/yXc8a/oSaGXseZacdsu7hcR7UE3/8Kqdu l8V0K0ewCWRmuF7smSTAWMIwd9vq3s4zvXaC/78OKhK3aEAXp5xRSO5gmMUwKxoiauau 7XFMNm/WP9juINQmyIT1v5mTTDwkviaAL3r1ulEE6THmfxSgi3C5kllJQlO8lZke7YF0 SMARMCQZel6oymkIqFj498UfgeUuELMCEbQWt3YthsyaOhQtc0X+bzwLksMZD4KMBC+g Qe0w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAU+DMmy91aLbnYhH8GarJ3A3VmGaS1C6zD5p1L6MNpDwUqHi94S Pz900xKkq5kto94ZdG3jvp4= X-Google-Smtp-Source: APXvYqw4JxnKcJGBMtDslCKv88TsTpw37z9qpgU9UUtHI+BgH122qWtKNMxlkB9OszPbttEZ6EpbLg== X-Received: by 2002:a9d:192f:: with SMTP id j47mr793721ota.230.1574800850293; Tue, 26 Nov 2019 12:40:50 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6808:49a:: with SMTP id z26ls3482942oid.1.gmail; Tue, 26 Nov 2019 12:40:49 -0800 (PST) X-Received: by 2002:a05:6808:644:: with SMTP id z4mr838344oih.139.1574800849643; Tue, 26 Nov 2019 12:40:49 -0800 (PST) Date: Tue, 26 Nov 2019 12:40:48 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <77829d67-ed64-43eb-aaf0-d673df419080@googlegroups.com> In-Reply-To: References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@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_1375_1157790901.1574800848759" 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_1375_1157790901.1574800848759 Content-Type: multipart/alternative; boundary="----=_Part_1376_1355740366.1574800848759" ------=_Part_1376_1355740366.1574800848759 Content-Type: text/plain; charset="UTF-8" On Tuesday, 26 November 2019 19:53:19 UTC, Kevin Buzzard wrote: > > What I meant by my earlier post was that the `=` I have run into in Lean's > type theory is too weak (canonically isomorphic things can't be proved to > be equal) but the one I have run into in HoTT seems too strong > (non-canonically isomorphic things are equal). > Given a *specific* isomorphism, in HoTT you get a *specific* element of the identity type. Let me say this explicitly: equality in HoTT is not truth-valued. It collects all the possible ways to identify things. In the case of equality of types, the identity type collects the equivalences between them (rather than being the truth value expressing whether they are equivalent). In fact, canonicity is at the heart of the univalence axiom: there is a canonical one-to-one correspondence between elements of the equality type (i.e. the identity type) and elements of the types of equivalences. So, the univalence axiom just says that the elements of the good, old identity type can be understood to be precisely the equivalences. You may wonder what the bonus of this is. This is the content of my last two bullet points in my message. 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/77829d67-ed64-43eb-aaf0-d673df419080%40googlegroups.com. ------=_Part_1376_1355740366.1574800848759 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Tuesday, 26 November 2019 19:53:19 UTC, Kevin B= uzzard wrote:
What I meant by my earlier post was that the `=3D` I have run into in= Lean's type theory is too weak (canonically isomorphic things can'= t be proved to be equal) but the one I have run into in HoTT seems too stro= ng (non-canonically isomorphic things are equal).
<= div>
Given a *specific* isomorphism, in HoTT you get=C2=A0 a = *specific* element of the identity type.=C2=A0

Let= me say this explicitly: equality in HoTT is not truth-valued. It collects = all the possible ways to identify things. In the case of equality of types,= the identity type collects the equivalences between them (rather than bein= g the truth value expressing whether they are equivalent).

In fact, canonicity is at the heart of the univalence axiom: there= is a canonical one-to-one correspondence between elements of the equality = type (i.e. the identity type) and elements of the types of equivalences.

So, the univalence axiom just says that the elements= of the good, old identity type can be understood to be precisely the equiv= alences.=C2=A0

You may wonder what the bonus of th= is is. This is the content of my last two bullet points in my message.

Martin


=C2=A0<= /div>

--
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/77829d67-ed64-43eb-aaf0-d673df419080%40googleg= roups.com.
------=_Part_1376_1355740366.1574800848759-- ------=_Part_1375_1157790901.1574800848759--