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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qt1-x839.google.com (mail-qt1-x839.google.com [IPv6:2607:f8b0:4864:20::839]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0c7cdc3a for ; Tue, 7 Jan 2020 22:11:40 +0000 (UTC) Received: by mail-qt1-x839.google.com with SMTP id x8sf745810qtq.14 for ; Tue, 07 Jan 2020 14:11:40 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1578435099; cv=pass; d=google.com; s=arc-20160816; b=uP0U9KBH2InQsUGmNRYL+/wUCpBNHtpH/AsjjSLOmRk2ZlLkiaf6OsNEaKxNdKrhVz uHJ2Fag/eeIUZyWysKpE9w1HPRGO3wDf0hWs7UaF4CoqiONioysRfp6q1PiULX2vC178 UVTSjIGXlk4Ef7hoG9isBajZX0x1s7RjSGO1eiQUnvc0kvhOxbb2vmMpDiyhlfJtvvYf DpjyaXv9wDV5aIhzmVdkqLrWSzU8tUsUvaadUdhTck0RKsRzvywiMSGNhr/c1qdlt0Wf NvDdkW1w1a0dnhjryTL8qlaMiyLrv1huqkjRcSGPpz40Ga+y/q97LzjGwfk4KMJgwG5P M8rA== 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:content-language:content-transfer-encoding :in-reply-to:mime-version:user-agent:date:message-id:from:references :to:subject:sender:dkim-signature:dkim-signature; bh=DxvC6bdMRtJZQWMRs5no9zZDGX7JpisTAH8aSahlwTo=; b=PI0mYQkULAzz4vH8JokJgoQ77DDCAvqiT4PPVu+bq1YasPU+TRry9b186KyKCUxzNs PCIlfXDws4KiiOZ0Nu3xual8WzrJUVi2HoRx453/XgtLYcNummkmd2tUCb1f/j6/oaHl B4DygEf3ew2Why+U5Q2qVqBXX5+hZGkip5Qa1PCHqBreqs87XGgyPd/n25TfkCZuWEsP mdx8pYuwhHCZ5OImayScESVDwz4/7ljlCSR443vygBxS3Bl6yDLcjmy9tIIg7GAjcMim X+7cEWvJUWQajuZ+zWZnhQ0TJtnZS+pjObnGVUMyRu2hpHHkdH2bck/v5idfan+7FQul SraQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=f0Ok7cQu; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2607:f8b0:4864:20::b33 as permitted sender) smtp.mailfrom=sojakova.kristina@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:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-transfer-encoding:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=DxvC6bdMRtJZQWMRs5no9zZDGX7JpisTAH8aSahlwTo=; b=Jcqb8tNRYUQerh1+AqXPpbbFjCaqR/5Iqzuj2Rw3jHL40UFfcfi+SGr2OfTvEZaDIq mQBv5oR1o8xLNSQcylWyv3lnp9BhrqyO5Cw4ffXXoRV+1I98GyaJZrEXyk2Xi27nIudB uwUrMcMIkkJIBjPJ0OzlG1sX/YEoBNYPHRUWFzOimEIYj2vA45Oahc1pRyZu6OoNPfBw AYRUa0oFrJHNziSqrOZ4/8cHDOjs1b1G7SBHtORDzGyaYb7NuAFFJwp6/HiabJP01IV7 JR6PEfmKMxAqm7ITpE1ndZnp3LySwIBdzznghyOS8iegIWnfk7ttHTV8o5CU4PBjt9MF Qnpg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=DxvC6bdMRtJZQWMRs5no9zZDGX7JpisTAH8aSahlwTo=; b=pPftNEb/jkVtADUsCOKVhVFGO+7UDSwNOFJK7rZsa8d5yTGRLFLv6lsHFmM/RrP0aO N/QFAxj4cd1qYD8GE/l1HK4w76GWLhpwqlz/lJmnH12WYPb1RVmaus6Af/hfIqIwjKNd 3BRLIBluYOnD5pARuteFuC9YmWn/jfVcCwkooL+jinBicyvR5df7+jnT6lTVROcUJxZL WVO70xSZvt85ZQ9zuADAqbkmquiAv4OoJCYT+9CFR7A0DO6U+Cc1d+f54JTP6FdCvoXm ht/4PfWkth96Bnl3238/9YSbaNNXHQRgaMRdMrqJv+jvnbgMH4vsZ3T/3/8LAIAEgQ3w azgw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-transfer-encoding :content-language: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=DxvC6bdMRtJZQWMRs5no9zZDGX7JpisTAH8aSahlwTo=; b=IuvGyGK430eCfIKBOhOeaXCSCApkBXsDpr05us88YIsQH4CAf8io4+wl2FSSvfQRML A2QZTIn81oPkZTgW/sUlHFe++L3TyKmEsCTpGxLn86Sxbj+5xr3tcHHmNJ0tJXv5+FYI rtE7Dm5o6i5K9IiI5aGPFx9caN9ywaSTRJN2S1Q+wPymsC3Jy3jocSRmSpHs8xuNpw+3 LnI9Wk+Vd94EMR5q7IsM+Vvcg1jaCDQ8qwusAqpyrmNRkeo20ByTHOxZh1MYf+2bAD2l YeU4+kpP98Vk4joPohix7fyaYRm09s8FsGX8tm6g7t58ynSXzSz/gmMbAzzkazWlFCby WeWw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXNxANOK1x1Hxj+QOyqiL+ZLqTohkWS41ASPpusx1WrVns4tyPf MX3L+0+ODeL/F01yGgA1zeE= X-Google-Smtp-Source: APXvYqwJDqGBul7xgobZGTRmWlYJ5U8qubaI3yIecJKz7WmhcTmzyjcVZIWHvCZVFHgmoJK0X+mwZA== X-Received: by 2002:ac8:5457:: with SMTP id d23mr954064qtq.93.1578435099517; Tue, 07 Jan 2020 14:11:39 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:4c88:: with SMTP id j8ls387338qtv.14.gmail; Tue, 07 Jan 2020 14:11:39 -0800 (PST) X-Received: by 2002:ac8:383d:: with SMTP id q58mr1005148qtb.45.1578435099179; Tue, 07 Jan 2020 14:11:39 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1578435099; cv=none; d=google.com; s=arc-20160816; b=mYBXfO/V8fAhMZusdQR9s+9AF1T5zEOTBvbWdPNiKmYBve2fBvWCSsZDZ7Wq0tbE15 vVd1JQnOZHnZ2bqQrB8F1A/GCyHiAdQBl87ts4Bezlj0fnuICPaFuUExjK4ya9q1fax2 TaFTMwF/M37ktI3ydJcxPxdVj3oTIPh7YOzvorEUBdsF/TfiFGY+nsEMMJKmJny61n+x qOIrqHV1wqLHzX92433JpbYHQzijhzqsQsnI8OppQx+Nspa6GWBGKsjFbGyKxZsnhG96 61owUH/rOIRaZ5bdB43D5QhRR7mThfSVEQnEDNzcZwOLfXaOGnuvseIy/l5JYFBqpEIs wvNA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :dkim-signature; bh=chh5vhCr2k5tqYE6B+WFVbnnm/y5Yqj5tOQv8xSY6Iw=; b=PhJueEP3njBlacDqbS0Ud3vLKBS9lQSY2z2i+M4IvW5o4JLdyV2PrboZPhePYC5dEC TDVPw45TRzRO1D8hBMoxaIts0S0xRfx2M0KPYJPYtmgMnyGbXvwjGkkGoXeZldS9R8V4 Ji5YwTCL2l7ZwZ1nKZ6sAqHbNW+nntpP5LzFBm12vnw8UA4S7daaOIH/vM0elcEpMH7c qrzmUqFY6VnnMHbtSpPjFqupj0w/j6mVgoehz8A+2ixBPUZJn8s824niD4ypubMTd5CE sp0tBrAuWhqODpFtjnkTF4gfB14lV/OzhsK1GjCz7nIlVgpAhtDysE/LtU1nCp+2GRRS aDTw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=f0Ok7cQu; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2607:f8b0:4864:20::b33 as permitted sender) smtp.mailfrom=sojakova.kristina@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb33.google.com (mail-yb1-xb33.google.com. [2607:f8b0:4864:20::b33]) by gmr-mx.google.com with ESMTPS id d135si49161qke.7.2020.01.07.14.11.39 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 07 Jan 2020 14:11:39 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2607:f8b0:4864:20::b33 as permitted sender) client-ip=2607:f8b0:4864:20::b33; Received: by mail-yb1-xb33.google.com with SMTP id k5so654571ybf.8 for ; Tue, 07 Jan 2020 14:11:39 -0800 (PST) X-Received: by 2002:a25:8289:: with SMTP id r9mr1516788ybk.162.1578435098601; Tue, 07 Jan 2020 14:11:38 -0800 (PST) Received: from ?IPv6:2604:6000:1403:3f4:c166:2e47:27c2:7646? ([2604:6000:1403:3f4:c166:2e47:27c2:7646]) by smtp.gmail.com with ESMTPSA id i127sm420640ywe.65.2020.01.07.14.11.37 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 07 Jan 2020 14:11:38 -0800 (PST) Subject: Re: [HoTT] HoTT with extensional equality To: =?UTF-8?Q?Rafa=c3=abl_Bocquet?= , Homotopy Type Theory References: <8de08372-b17d-c153-73ad-4cd8b6c49758@gmail.com> <7d1235e5-76ac-2a7d-9317-21d30f6973ad@ens.fr> From: Kristina Sojakova Message-ID: <60639a49-a1c6-0cfd-0bdf-65ad45b14e24@gmail.com> Date: Tue, 7 Jan 2020 17:11:36 -0500 User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:68.0) Gecko/20100101 Thunderbird/68.3.1 MIME-Version: 1.0 In-Reply-To: <7d1235e5-76ac-2a7d-9317-21d30f6973ad@ens.fr> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Content-Language: en-US X-Original-Sender: sojakova.kristina@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=f0Ok7cQu; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2607:f8b0:4864:20::b33 as permitted sender) smtp.mailfrom=sojakova.kristina@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: , Hello Rafael, Thank you for the reference. I browsed the paper; it seems to me that=20 the theory does not appear to support identity reflection. I am looking=20 for a truly extensional form of equality (in addition to the usual one),=20 where equal terms are syntactically identified. Kristina On 1/7/2020 5:03 PM, Rafa=C3=ABl Bocquet wrote: > Hello, > > I think that the paper "Two-Level Type Theory and Applications"=20 > (https://arxiv.org/abs/1705.03307), whose last version has been=20 > submitted on arXiv last month, answers these questions. One of the=20 > intended models of 2LTT is the presheaf category =C4=88 over any model C = of=20 > HoTT, and this presheaf model is conservative over C, essentially=20 > because the Yoneda embedding is fully faithful. This means that we can=20 > always work in 2LTT instead of HoTT. > > Rafa=C3=ABl > > On 1/7/20 8:59 PM, Kristina Sojakova wrote: >> Dear all, >> >> I have been increasingly running into situations where I wished I had=20 >> an extensional equality type with a=C2=A0 reflection rule in HoTT, in=20 >> addition to the intensional one to which univalence pertains. I know=20 >> that type systems with two equalities have been studied in the HoTT=20 >> community (e.g., VV's HTS), but last time I discussed this with=20 >> people it seemed the situation was not yet well-understood. So my=20 >> question is, what exactly goes wrong if we endow HoTT with an=20 >> extensional type? >> >> Thank you, >> >> Kristina >> --=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/60639a49-a1c6-0cfd-0bdf-65ad45b14e24%40gmail.com.