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-lf1-x13d.google.com (mail-lf1-x13d.google.com [IPv6:2a00:1450:4864:20::13d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 7b046a89 for ; Tue, 7 Jan 2020 22:03:23 +0000 (UTC) Received: by mail-lf1-x13d.google.com with SMTP id y21sf232530lfl.11 for ; Tue, 07 Jan 2020 14:03:23 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1578434602; cv=pass; d=google.com; s=arc-20160816; b=ft0Y/XTG6DzAFdX0kEqIHITnRklFxRx59ArQZBhjVoqe+yGaTKCj/qT0Nz2vcDYGzi NOulWjotNwlPKQ3pceySTTnp5sxe4cuOlU6olaCChNrQQO5+f9EMNlocpOhaU/ICI1My DAobQtUQsSOptCqDqAJFZN+d4B9nfSEvlYZ4KkxwDzZr2IKxmXCO0AaAgXY/we+FyzXq F+Wrebv1TtXbDfSDrWugg5TxfGcN0OWah2p2WzlsEh/gpx13Dg0mFLJOj4jmvlEG39DS EK4jS+7Zgw8t7zqpcBzscXXzwx7xx4kASTObPYNxymgj1SJDrgNXUW0b8H3fvL6qE8z0 5GtQ== 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=Foz0+VZxpisOSArprzppHRaFbals8A/QlJM4wKX/HeI=; b=cpzCZybzVZTj5ADrkgTUupnAmZLXEk0RcTrbMYtOlfGaPP8+I6b8gCRzkO9nZFkfZ+ mrM43XYsN1/wUoOJKNpfE3OZbhGawhegOGnAH4nCNQFqcENYWw60qpCoPc63hz3cI2lX QP78pMZOeyAgnBt///zebFLXJAZMk5dZ8HMrQzR9bci1nhmYNrzmTRD2EqNiqnNL3JEA aaBJmUXj1D0EfnW1H+RIB1PUzCZjIX4xhLYVaDbhADlG/wIn0hwrIuQq2twQbFPFIy22 XYx/GzQkohCN4AWZJhNlHS6k4NMx9EdqQR3VrA23ddVTwDKHJMm7npeuCUmEYXKB9RCE iMRw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@ens.fr header.s=default header.b=kQOCSi4h; 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=Foz0+VZxpisOSArprzppHRaFbals8A/QlJM4wKX/HeI=; b=kP5l1nrx2Nz9XKUizTZT48Tz2aE5kzObkDIVL/FIhbv1fzUdVLuKE4eQqmYb78nlWH 5cdjKS653RcYT5PSIJjlp6HqqNJnUOBneBSa5R1KiD3ISJtlvqfouMfeWZk4mBRWxrlI dOcO+pCOxHh3H1sqjkk8bp/3ZsC+6fkXggDN9fS6Dpu1Zm5Sw1Bx0F8OnXrA6b7yA7IU xEZZGrn3qAdqGEq9pG7nxZ9YzAof3xc8rf8XVlTvFIwwli6FpO+GR63za/p0nz2cuUeR hMWsmXer0AOECcqh75p0mTAAXVUVFFDy5bglAl7RSc0XWHyPDnPVc+M+MRteuJROqdxH AiSQ== 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=Foz0+VZxpisOSArprzppHRaFbals8A/QlJM4wKX/HeI=; b=O4xhJt5l+HcjLYQwzDwG6egK+C67xQZVk/R6tsOlCuFH57xfqFtFRAfO4ugiyKeNd+ witWNEFiCCczuTWucvmBtewI0HBZ6YdvDU1BWDNM3M9xIhHA2uED1iKU3lsTHcW7DTSx Hy6/Fn67lEvFfBq0c5o6sCGw0WxqmQHKuYtS7C6yb78VMhY6qKbRftn/dec2rL0pyMrm PLG37iagV+cPDOQWDGwVLefdaMOnk7UxLxJI57xmSrNnJvh60IOb/30h/nkv7WxVofqw ccGucCGhevJFH0OOcdm5h+cwTkizqNe/lw+l2X1v8fsyJPOj8fK2rVnrseHLooqfB4gL Sm2A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV8EeTOQ/kjIGS4rJt/Swfurd8YtcFjb+1+pNveBhYhwhnMA9yj aTSqYW2aEO8Dq8SmlXU6d10= X-Google-Smtp-Source: APXvYqwPQ6jFbezBwH0Wq6sdF/jcNy0BhBeE310iTVBAA8jHdIKL9ji9lES7GaHoT2NCjByJSRxjxQ== X-Received: by 2002:a05:651c:111c:: with SMTP id d28mr999338ljo.32.1578434602149; Tue, 07 Jan 2020 14:03:22 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:b4e7:: with SMTP id s7ls123210ljm.10.gmail; Tue, 07 Jan 2020 14:03:21 -0800 (PST) X-Received: by 2002:a2e:b1c3:: with SMTP id e3mr920080lja.137.1578434601459; Tue, 07 Jan 2020 14:03:21 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1578434601; cv=none; d=google.com; s=arc-20160816; b=X4EY1LutVGoSavZ7QW1KtMMjN8EtUqQFvV+RdT73nOnx4LMvMaPuvD6xC4Z2JzwMPK 25xAzgdmPoqxvl43CqKp//3Hi34Q8TD9C5xmEKL6EYce0FpTk1Zh9qfyciR8dLiJFjrM A8uJznC5kZ9F5A7z1QEEOa8utyDDDdrxoNxAiyxfkS/cwwAjBXapYjgrYQQ6NYG4OW+Y UspbEGX9q2EgbRIj5EWhFik3/vYwZjzdn6LkQsgdi8xLvIc0aBybgNN4r4CVa/D2JiHj BsYPveQIcuYYSyxtjP4kR1GhWKi/X8fNKx9UjKz84D4Py59/qBh+e8PYg634qQoyUOta Jehw== 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=3xDPuokszxnf4jSk+zxUNMDU1bd/LURiubzn75rBwgs=; b=dNiodzv+ogfH8tVGz/TVAMA9x9HRpax94PxJyTWcJBNyVWEPfs46qKmtyCFCw66OOj iTm0uk7YvEqS6V6yV1h1lxfB6J1Smsbf3PSimFoza5STmaP8m6zJM6SBhPBJdKf0/mBy dcuq1wBebCNTjXr/8IxPwE5gHmMoYGE05iWCoJ6eCYtS9ZahOWMswAZIlODQ4pqKar+c bgl4XTi2oclvywnREYPw38w6Zp6KOhz2ZOlKbX3GuE9RZegMGk8IOfmA7MDF1f2vE1Fi +aNTHiYz9gVdiB0mIl5HM0ujYuBFBrQQfonAVkBgAZ991MakN0WUf07+1JXpRDTjgHUX apmA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@ens.fr header.s=default header.b=kQOCSi4h; 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 v16si38135lfd.2.2020.01.07.14.03.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 07 Jan 2020 14:03:20 -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 007M3ITP025570 ; Tue, 7 Jan 2020 23:03:18 +0100 Received: from localhost.localdomain using smtps by clipper.ens.fr (8.14.4/jb-1.1) id 007M3Hg3029292 ; Tue, 7 Jan 2020 23:03:18 +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> From: =?UTF-8?Q?Rafa=c3=abl_Bocquet?= Message-ID: <7d1235e5-76ac-2a7d-9317-21d30f6973ad@ens.fr> Date: Tue, 7 Jan 2020 23:03:14 +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: <8de08372-b17d-c153-73ad-4cd8b6c49758@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:03:18 +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=kQOCSi4h; 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: , 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 people=20 > it seemed the situation was not yet well-understood. So my question=20 > is, what exactly goes wrong if we endow HoTT with an 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/7d1235e5-76ac-2a7d-9317-21d30f6973ad%40ens.fr.