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=-1.1 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-x33d.google.com (mail-ot1-x33d.google.com [IPv6:2607:f8b0:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 93ee9aad for ; Sat, 9 Feb 2019 11:55:57 +0000 (UTC) Received: by mail-ot1-x33d.google.com with SMTP id g4sf5731052otl.14 for ; Sat, 09 Feb 2019 03:55:57 -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=7rGuBdLrZPyAmYYeBWwpGt/utY9QSWZMbji/AVO2VaA=; b=Sfz4b5A2qgJmbt+FtiTYkVTrZttisvtEcYUyJodYcqlujGn72xw0wq6Q716dYe64qG /jZsSj1m7tBu2FDKOYwu4g9i6PbOa0V+9nps1dOztFp8vqKjuUCLRM9it5ZQQY0/kUFn f4YibU6uwBgNJu/eKvsDWPgjNE7m/wC6+N3mWXF1Pv6q1wL+stQZ3xYRYLBBFHQSLycW JErrIldmU1FOZkpQvPFckxsUDumWd64r+n2/E6pxZQ7Q6BKbfCF3Ju3n6K8LvrLS/xs8 VhIKpHLyr6i4wUk6Y58+ituKg9ROB55yKOU0wpfXQCZjvI8lPxEpiExpAhzPLgZrAuA7 7aBA== 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=7rGuBdLrZPyAmYYeBWwpGt/utY9QSWZMbji/AVO2VaA=; b=Pq2YDo9/0QyyzXwhD1RiHO4YqWv8Tr3P95WDawdFx1cF2MYooox/XTvHAc+pB1kKuY mRW6WO058+JFF8dpu6Vn8ujyG03xJgv/KEhk3E9q2tFciyKStbwp5xELRwGxgsDtvrZj jcy1Hyzf0hLub+sDiXSf3AcZOPNGX8uH0SUZvO+FuHzpmfp3fPC+pS3XqDZO2NX2YQKj tU3zTpNmgbAndOQx4zGqpx9jMsT/6nx9xu1xpAejL90aJkOdGUFLgMIzbbI5jX7vCj5Q aLX8DKKlaq5xClnv+StYw1Z6LyQni4EreLRzNobKATzizV79r769BHj/MqrDqnt+EHrI f8hA== 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=7rGuBdLrZPyAmYYeBWwpGt/utY9QSWZMbji/AVO2VaA=; b=jbcG3rhp80Z7iQAp6m7wmz8mM2ldnE1AhD+Ob5tkYxZG/q5GySNKqDIPSNYUkYXEik 2bjmO6dP4mukzHcbKNwVYpHVjg8qjoWzeugoVr7UCyxr7xmOGRNXq487zxt6S7np+DaH Zxx4AWdNMY4z181etP+0lH6t5lfplS3V0B1L1XIsnX12+rk3WVVsZXK+RfFQNFkcESqt 6Bx9ToBJJ0Jdw57uGBcy0U7DvTEMDJVDFkDtTStk57cgSTmCYe764WBwfnrrbsiwMIpz c+OxhE+5IG0QuBxp75B1Y0F6La/pHo8H4hO1PwCD1k0nJJpUWjH6e76Cwga/KMW80I3S HI5A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAua0rr4KHScbU5i0RjDGkUXOjxUpkrgNxdEfRR6th/RGUpwquP3R GgxS461dqPOvNt9q32275bM= X-Google-Smtp-Source: AHgI3IYD4odorJFIUl3pyiXaIAVHjs+PbZVxjD848VbpiSIOPMDVeDb40t8UXvyoGwPBgqyL+cx0Mg== X-Received: by 2002:a05:6808:1cd:: with SMTP id x13mr47464oic.0.1549713356479; Sat, 09 Feb 2019 03:55:56 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6830:146:: with SMTP id j6ls690157otp.10.gmail; Sat, 09 Feb 2019 03:55:56 -0800 (PST) X-Received: by 2002:a05:6830:130d:: with SMTP id p13mr108327otq.2.1549713356161; Sat, 09 Feb 2019 03:55:56 -0800 (PST) Date: Sat, 9 Feb 2019 03:55:55 -0800 (PST) From: Felix Rech To: Homotopy Type Theory Message-Id: In-Reply-To: <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> Subject: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_738_958906980.1549713355537" X-Original-Sender: s9ferech@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_738_958906980.1549713355537 Content-Type: multipart/alternative; boundary="----=_Part_739_1178245178.1549713355538" ------=_Part_739_1178245178.1549713355538 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Wednesday, 6 February 2019 05:13:35 UTC+1, Anders M=C3=B6rtberg wrote: > > Consider the interval HIT, it is contractible and hence equivalent to=20 > Unit. But it also lets you prove function extensionallity which you=20 > definitely don't get from the Unit type. > I have the feeling that function extensionality is special in the sense=20 that the proof that I know of, as well as that of function extensionality= =20 in ETT, relies on the fact that we can replace judgmentally equal terms=20 under lambdas, which is like function extensionality for judgmental=20 equality.=20 --=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. For more options, visit https://groups.google.com/d/optout. ------=_Part_739_1178245178.1549713355538 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Wednesday, 6 February 2019 05:13:35 UTC+1, Anders M=C3= =B6rtberg wrote:
Consider the interval HIT, it is contractible and hence equivalent= to Unit. But it also lets you prove function extensionallity which you def= initely don't get from the Unit type.

=
I have the feeling that function extensionality is special in th= e sense that the proof that I know of, as well as that of function extensio= nality in ETT, relies on the fact that we can replace judgmentally equal te= rms under lambdas, which is like function extensionality for judgmental equ= ality.=C2=A0

--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_739_1178245178.1549713355538-- ------=_Part_738_958906980.1549713355537--