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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,UNPARSEABLE_RELAY autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x539.google.com (mail-ed1-x539.google.com [IPv6:2a00:1450:4864:20::539]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 41e7b51a for ; Tue, 7 Jan 2020 22:18:06 +0000 (UTC) Received: by mail-ed1-x539.google.com with SMTP id n63sf471622edc.20 for ; Tue, 07 Jan 2020 14:18:06 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1578435486; cv=pass; d=google.com; s=arc-20160816; b=WldJTSskQU5Y+2xhI0ZoRYcnRvveH3pqfDtoINIArFbBkHGqjL1TtQG+8cABc0GVF9 iYksTrHQLs8Elni5Z7CEwDw6a7Mn8GM/BkPdp5bm1UlrF9aa9kcmTY72gn3MZ0daNUvj vMeVgZwD3RJqJ9f/kQ6XgM/bIxi6eURiC/lbYo+UVd3IJXkt+z21RQUc4VOEDcLU+twS zuvGgwnWw6vvV9jvxFaVPxt5/cWnrhHm0x6cUhA3GImZ2fyP78J59AaB/7PH96yOYSlr MRdF5fPD5QPSuNR9H0NoiBeF81dLTEUjgjh3j4iOmK2/O8EyR7tpLKyP3Rra99YQSv+1 C4gg== 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; bh=WZ3dhcPAYkbP4SqpjV4CT1/UIxFxWKCbsKVeg7Y5nQg=; b=Ogshdwo/qgwlnr7Irmounlcdh5IhE56Y3dCD1iwrtT37rqDomOMxZJCXTz9ndubL3y xHldV3t4L8VOE23TCJr/5JDlSftNXrtX7RCG6moPcHc+WFjS5LeofeTIyUHfCadRZXHk HXp0OjZU5rULDVeOyuezR8hRylfkHhQ12Xeeo8QF4ktqbiDEC6jjEY/3O+nRkgpaFM9S 5PxnXVHRS+r9vRHgX29z2opAwQ9oj8JooSC3JzNutxdWS5tHI6t8z2n5bwC7QhykhI+R KnL+vjRXVrrD3xeDGFCNsxD4YVchqXXB2riOsNXVo7H5eIqBErrNZjascUoc8RmHNU2S AY+Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@ens.fr header.s=default header.b=a5dKMrAa; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr 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=WZ3dhcPAYkbP4SqpjV4CT1/UIxFxWKCbsKVeg7Y5nQg=; b=pHksDlBYXJBU1Xcw4R8B+YwhbAwd4yaHrRFxcXIPJY6nnnoDWaDMIQHaMJmeFnifHv JxlzwesKQrhNmC2e/rdZyIwZEWEkPtShY9s3S+dZOvWF0/8Opaz23IkPh7S6U2eQ4qS8 43LNcJoKXQm67wE5jlgAEeqTDLrXNdcj1NV4HJba4Z/730fOJ2WsyQv42Z0mdp7UnPj+ 7EUeeyXHMCCmLj3qzd5ubcU+lprvkE3xU357MekuLP9yIEFVT0FiZvdUpsSpnSQuDpnO FDpGiwDSlZk0IHyNiOF35KHNxT7UJabiFMCPs4j9xfE8lN/NkcOLrMfFGI0fHrY7+GXP 9FdQ== 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=WZ3dhcPAYkbP4SqpjV4CT1/UIxFxWKCbsKVeg7Y5nQg=; b=QLdpmSRSgn3vmMIXQTGf4UViZrl32x++Czcc5vHOwYV+8+9s+xnX48hLp/69OVC5Lf YinFrblptuFSlfUybn+VEgadRGEvu/Tq335n0gKEcbHxFziVjHVX968/gV0TQsF3DSAh PztIWXOuQHWBr4xXdrhNmhHqmQrizZH8y+O0qnLlG6/clpsFOk9l7nlHJmwdGRlxLXSZ TnaGoZTluz8zjNxV1mBPdXzWjR0IrVTtdLKYYbU5PcV69H8WGtAuPVHC4NDG7MjHHKgy KynE/D4N+BxaTl0OrfRdoxxFVrHWLXvACJVPqr12TEALNhGVkhUrLsG7BtWqxY3VfPWN 0KzA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUnCpxGtAQTL+VX0NYwjedCIyCuHy3Xy9/c2/ETDYKJMvQk5ZCX lelV+peHsnhXBnSMjsAas78= X-Google-Smtp-Source: APXvYqyAWpRwPLLGjFru3BICp2Q7uy3h9qKxptHxEhfICHdEJMJab2Dx3g7KIAJ+L8bleLYC40KATg== X-Received: by 2002:a17:906:b219:: with SMTP id p25mr1764989ejz.36.1578435486142; Tue, 07 Jan 2020 14:18:06 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6402:897:: with SMTP id e23ls290232edy.12.gmail; Tue, 07 Jan 2020 14:18:05 -0800 (PST) X-Received: by 2002:a05:6402:1a5b:: with SMTP id bf27mr2276079edb.243.1578435485613; Tue, 07 Jan 2020 14:18:05 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1578435485; cv=none; d=google.com; s=arc-20160816; b=n7AUYDrq8x+VKcjBWJlqw6pPKxANJWcsr41/T/EY7e7wpViBEBdZFyo8z/cuApMcyR fXoMEULplcZnNE4IO3/nzlkzh/FS+UNS6TIjGEsKvh3JlDfTuXXVn8az2o62yaH/Uy4H kYnw11FJQRfmV0/GVPwQpFEIYyQEvTZ9WJ3hoZEvFEWqVQG2jnKRLzYdsbbTg33KXR6X X+R7GLhWYP1fuodC6rJp1No2QNDvaa4i+Ky3lNDj0pgeN76yC1PKTCjABKKPla/+xRqL gBOpD8u1TLg7YLDTuEfd2yIkHYtCVXuR9uzU8Ab+T0fhpKPj1TleskS2xASOobPTUyDe UMFA== 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=CH8xyp2g5UrM5aWcXwD/Yv6f2fGOyQobaZrbHsR8nCU=; b=Pnl1wlV8urfOwl7pBUrhYSOLVWLeqcYFsDQVeL1dyh2sucod+Z4+T8yiC/S49T1FSe VyJV7sfHdNnBEKIexUQ21HyfCqWO8f4f9ia4euqAGcllMLp/uQh+NQRzYVAg+bJMesIR UtVkOOj1kFBY0+y8p0yeGG9zLa8D+7IR/k2hmE+KNLT4vuc5CuWTWlpIwNYMb78liY6T Je0GrVV4U9sHpMIiTnjczW63roBqgD5mzW5OdkXIqNUd8Cadep0+6a5n8J5GASF7gGxj 6laF1gXmpoFJozCKG5D3LsKep5au5Agqua8AkGdOM7LlBRrPmd0Gi5rJv95lIrIc1+lb gLEA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@ens.fr header.s=default header.b=a5dKMrAa; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr Received: from nef.ens.fr (nef2.ens.fr. [129.199.96.40]) by gmr-mx.google.com with ESMTPS id x18si49437eds.2.2020.01.07.14.18.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 07 Jan 2020 14:18:05 -0800 (PST) Received-SPF: pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) client-ip=129.199.96.40; X-ENS-nef-client: 129.199.1.22 Received: from clipper.ens.fr (clipper-gw.ens.fr [129.199.1.22]) by nef.ens.fr (8.14.4/1.01.28121999) with ESMTP id 007MI4am029120 ; Tue, 7 Jan 2020 23:18:04 +0100 Received: from localhost.localdomain using smtps by clipper.ens.fr (8.14.4/jb-1.1) id 007MI4t9052198 ; Tue, 7 Jan 2020 23:18:04 +0100 (authenticated user rbocquet) X-ENS-Received: (catv-89-133-37-198.catv.broadband.hu [89.133.37.198]) Subject: Re: [HoTT] HoTT with extensional equality To: Kristina Sojakova , Homotopy Type Theory References: <8de08372-b17d-c153-73ad-4cd8b6c49758@gmail.com> <7d1235e5-76ac-2a7d-9317-21d30f6973ad@ens.fr> <60639a49-a1c6-0cfd-0bdf-65ad45b14e24@gmail.com> From: =?UTF-8?Q?Rafa=c3=abl_Bocquet?= Message-ID: <563bb6a5-7603-c59a-5943-6f925e56b2b4@ens.fr> Date: Tue, 7 Jan 2020 23:18:01 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.2.2 MIME-Version: 1.0 In-Reply-To: <60639a49-a1c6-0cfd-0bdf-65ad45b14e24@gmail.com> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Content-Language: en-US X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.4.3 (nef.ens.fr [129.199.96.32]); Tue, 07 Jan 2020 23:18:05 +0100 (CET) X-Original-Sender: rafael.bocquet@ens.fr X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@ens.fr header.s=default header.b=a5dKMrAa; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr 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: , The intended presheaf model supports equality reflection. Martin=20 Hofmann's conservativity theorem also implies that most type theories=20 with UIP can conservatively be extended with equality reflection. On 1/7/20 11:11 PM, Kristina Sojakova wrote: > 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=20 > looking for a truly extensional form of equality (in addition to the=20 > usual one), 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= =20 >> of HoTT, and this presheaf model is conservative over C, essentially=20 >> because the Yoneda embedding is fully faithful. This means that we=20 >> can 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=20 >>> had 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/563bb6a5-7603-c59a-5943-6f925e56b2b4%40ens.fr.