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.0 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-wr1-x43d.google.com (mail-wr1-x43d.google.com [IPv6:2a00:1450:4864:20::43d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d31e5552 for ; Sun, 17 Feb 2019 13:29:37 +0000 (UTC) Received: by mail-wr1-x43d.google.com with SMTP id f4sf6517909wrg.9 for ; Sun, 17 Feb 2019 05:29:37 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550410177; cv=pass; d=google.com; s=arc-20160816; b=c0W74cnzr6WZ2YJRaNcaOdlqFbDcThfY6hbsmUT0Vim1E7hqowBR09G2RTi5paa2WJ Awj/cPMwrB3JEKSZ/nMHr8gIpQYQqA49HJ0/PaCR58yMtyEjlg6KdrbTMedzmMTFpqfz NdXH9h0uhM0TqEI4wM0yu8vivmN6IjScCBMv+6YsY4iWIgy/1Cu/K30PTT4wQb9uOvjH T1+4fMgIUbcd8Om361pF9qSGoiEj4XhxypFbID35uryqy8NAUSOIZ+HoBhxhuwsfJRdL oOzepdEYyrS5ByMV3UiCS7k3j8AtOsqUJJEYnARg9A62rKZp2xynDqPm3ZRfQARity88 ICiw== 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 :dkim-signature; bh=9ggNzk9lrlFzncIG96nJcY8pObEKIH/c/yPB80U/3YI=; b=lNdpMbw243u/5ztOxDEtOQzvP8xuYn6uRAyboJrUGcQMwug5BO0DaEiakIHo2v+257 sR3I83Y/h5YROxxAo/S/1IeZUTqI0aaeEH81AKp4nWIsmSY3nJ1/wGrvjt7mlCA8Q2tC 3qwgQHXW5X0SkWIb3mDoSoOsJ1fRjJ4ibq+Z8wJO6R6gCimKncftFe1ruIbhZL2Yq8gR vqHaJ21irCEeflOu27YMrSlFWTIWjynZjFohO4cJ1dzrbf9cJ6yANo52GFaYTfZ5G6EA EHUOftQrXnOjYbcA/0qm8QQ9oWA3TACoj0l2NhsH4x9YOhyp8T0y5RlRyU76g278jmge zCUA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="eS/Kw114"; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::132 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=9ggNzk9lrlFzncIG96nJcY8pObEKIH/c/yPB80U/3YI=; b=qk3G4djHA+6q4ax+XabY9pFbsOjIOmb1vekceHirxOMa9LIxDydiTk9oHh26XlUSIz JE8DQU5pMjioiLK5Kl/Cvr9bw5/VIfK2nCMbwfR49wg4XidS4zOpPQVuCGY2JDnEUOgy ac5JZXFkWiQc9ACiOLAzg974MyMDRp7qzjgipUfqATPjghVrwPlWXbKip75XMmX5q1f6 X6nkQ/wXQrND0/+qgXmoDBMw6VwID//hWa4TXtmpEezh/brOTqZCNKKOxmSfX221rPxj YF19jFkCae0EfwOT6ZMhYMBEKxC57eE7DlmDt9dJM+hgsdWaA9WBtuvzWmQXLwApbhSi Hn8Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=9ggNzk9lrlFzncIG96nJcY8pObEKIH/c/yPB80U/3YI=; b=fL4i+k6Gp1PxG63HkJ/Ym1VkBlHjIeHKWFfeAFuXT9LBwiBhF1hAwDAd/6ReGOGpRj gFbVjTMxq2DZv+yRXpGXF0a+gXwhVVMobVYQQUqwFdYTI2b3nx9ljt/mhbXFQ6izfPcp 70G5ROQgUusVLT/5PfZQ8yoBPuwJY/GoRfkIH/EtjJrWvrcwV+fqJda3mN6FmegI0bZv hQoWGldA239PlTjDDgVyF/l6CZduVIJLuGtQ0jv4tCyequ61zKFyp2pcLbVsX3KRSfIn cK8vPVgk7sVVSo3tsr1SyjFRwPZgsCtFUs0QSVQ59fzP3PJJ82D33Uh+4Q5rT7Gv5I0O Cneg== 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=9ggNzk9lrlFzncIG96nJcY8pObEKIH/c/yPB80U/3YI=; b=EMZC2c1w4FhUmqMujCsald/PB1Z1EmhadsPTDTtilo14SLo/tNFY3ehWOgriRRX6l9 m+Fgl4f2sPk0IEIZg3qAMwVdR5nVVWoYbGy0a3rohs3eq9pE6geQxsVa0x2puWsDE5fq FQjDllFMjfX2BudQNrCOyn6saJ63G1ZmPkLkEsUY3C+jB8qcgtUiiZTDJ+PDia7qR8BZ X5vbGUsZALGq02gIDGoCfs3OUYeMDhx+gm4zp84mwyQ1/2gp36FxsKwpf/j0w41SH+TD 094NNpr2DOd90EHYBAilIyHWaKy497s7epXm5jxVaPbmisgTKyJPaYoC2kuy83rfwCd/ kraA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaWsK30KOnOQHB5ylgsOyl2uNvDCSarfbE7ZcqJA8xiT3KapEyi td2Y3WkjHNk/rjCaD5ghEJ4= X-Google-Smtp-Source: AHgI3IaTM0tzd06GoMFpnKu7/0Fwr10W9OxeEvcaWYdNzLJmB3OsvSogP23fMEab4giPl9uCVy0PQw== X-Received: by 2002:a1c:7908:: with SMTP id l8mr21269wme.1.1550410177319; Sun, 17 Feb 2019 05:29:37 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:35c6:: with SMTP id c189ls1376734wma.13.canary-gmail; Sun, 17 Feb 2019 05:29:36 -0800 (PST) X-Received: by 2002:a1c:2d15:: with SMTP id t21mr321360wmt.1.1550410176666; Sun, 17 Feb 2019 05:29:36 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550410176; cv=none; d=google.com; s=arc-20160816; b=qmi4HVLMwWe2jIzTBZ37+Jvbwe3LR+AgrH9Qx7Ff2DVyBY6iuZa7+nI2dPyIMpv1gL lsRcAKzyFrY6wHuDvwVPDIZsGjmKhix+dojNG9lTviXHS3FhD2qR4YPyxCQ8/yHTBxFi hHw1VrjSIPwTnLLl3fxdwbVS96Rd7EPOYjGDop7ZvI6O8ByAbbYxo/kMWyHRdBVKNd9F nfkkStGb1mk+/+Yeza+hCaBOW/fD72qx/BoFUUh6PpU0GHvkiIVtpu4Xu4xeqfdX+ETU TAWwEGj9deewVvVDNItqzW2qwRyRl3Mjp0Gv3wn+DmZjEDnSj9gqtNpK0uEXXSt5CA+2 VmvA== 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=rgeSnzZAuSncXP0f/SyVLI3jLxthow832q9kvXWmcGI=; b=RmSY5jXkn/uSQSXJrKOag4y/aKwi8mNfPcql5l1UQwznTXQMtKBzN7XZcVMbN+sNM+ Ny0qKii6MB1iDhAVrMVVeJnnbIY5+zA+pkRUTnjMSoxlesOmWQtBXniIDi/sx0Ce3EPD +gOhZAXQow3oWhPVo177YofHO0VyT8Vs5C1T80obGTjxNZ/NphnuI95INbb057IgoAV6 XS4kf3paxsop6k7EgJHvT1x9HUKB1XVJuvfGQ23G0sPTkPk37k/ErV3esjJvnCEJKM4a 6J0FX7XHWCfd3UKgqqc9zqf/PzvDrmXJo5SX66hWLFJ+uXNyvjLYPCyZaZmRb1w2kLSU +zyA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="eS/Kw114"; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::132 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x132.google.com (mail-lf1-x132.google.com. [2a00:1450:4864:20::132]) by gmr-mx.google.com with ESMTPS id r15si251013wmc.4.2019.02.17.05.29.36 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Feb 2019 05:29:36 -0800 (PST) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::132 as permitted sender) client-ip=2a00:1450:4864:20::132; Received: by mail-lf1-x132.google.com with SMTP id h10so10115919lfc.12 for ; Sun, 17 Feb 2019 05:29:36 -0800 (PST) X-Received: by 2002:ac2:5303:: with SMTP id c3mr11606494lfh.97.1550410175924; Sun, 17 Feb 2019 05:29:35 -0800 (PST) MIME-Version: 1.0 References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> In-Reply-To: From: Nicolai Kraus Date: Sun, 17 Feb 2019 13:29:24 +0000 Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Michael Shulman Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000cacfc9058216ffad" X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="eS/Kw114"; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::132 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --000000000000cacfc9058216ffad Content-Type: text/plain; charset="UTF-8" On Sun, Feb 17, 2019 at 1:25 AM Michael Shulman wrote: > The supposed arbitrariness of some types having strict eta and others > not has been mentioned at least twice. However, I don't find it > arbitrary at all [...] In particular, the difference in whether > Sigma-types have strict eta > or not simply lies in whether we are talking about positive > Sigma-types or negative Sigma-types Since I've mentioned eta for Sigma in this context: thanks for this explanation, Mike! -- Nicolai > -- 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. For more options, visit https://groups.google.com/d/optout. --000000000000cacfc9058216ffad Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Sun, Feb 17, 2019 at 1:25 AM Michael S= hulman <shulman@sandiego.edu= > wrote:
The supposed arbitrariness of some types having stri= ct eta and others
not has been mentioned at least twice.=C2=A0 However, = I don't find it
arbitrary at all [...] In particular, the difference= in whether Sigma-types have strict eta
or not simply lies in whether we= are talking about positive
Sigma-types or negative Sigma-types

Since I've mentioned eta for Sigma in this cont= ext: thanks for this explanation, Mike!=C2=A0
-- Nicolai


--
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.
--000000000000cacfc9058216ffad--