From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.45.71 with SMTP id t68mr143233wmt.2.1487861853546; Thu, 23 Feb 2017 06:57:33 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.51.21 with SMTP id z21ls710578wmz.20.gmail; Thu, 23 Feb 2017 06:57:32 -0800 (PST) X-Received: by 10.28.127.146 with SMTP id a140mr236735wmd.8.1487861852674; Thu, 23 Feb 2017 06:57:32 -0800 (PST) Return-Path: Received: from mail-wr0-x232.google.com (mail-wr0-x232.google.com. [2a00:1450:400c:c0c::232]) by gmr-mx.google.com with ESMTPS id v201si63054wmv.3.2017.02.23.06.57.32 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 23 Feb 2017 06:57:32 -0800 (PST) Received-SPF: pass (google.com: domain of benedik...@gmail.com designates 2a00:1450:400c:c0c::232 as permitted sender) client-ip=2a00:1450:400c:c0c::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of benedik...@gmail.com designates 2a00:1450:400c:c0c::232 as permitted sender) smtp.mailfrom=benedik...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x232.google.com with SMTP id 89so23285429wrr.3; Thu, 23 Feb 2017 06:57:32 -0800 (PST) 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; bh=9QTMSqNvLLPW4p+RlrPNwkEMXAi5FilK6uRGGjJEsyo=; b=a5E1BssnhzfvdEUPbDxPcrB8QSasbfQ2EJpAnA0m7n6Jh52M5+js2fSn7Kn7jZVFoa LgDDBPejNhGS7odwofTnycgf22N+YJqWITRvsb8xxHHc501GybT5RoL1HxDHhl7pcy7x Er9rj/PkjfN965HzlX08ml0jnojxLPABLugYxHyXFDxVugngkQfMowFKwH9thJMiWCl4 lMIA0hU0hlvDBaTI0Za3+3xq7mFm4dWmtAgQq/pLRZ8+IVlts3jRcPX/0V7tLlqzuF1Z A7PXDKC7UOGng/etZfV6wGJkR7JScmVM0d8OTVML0JJrGixzQZY2kZiEUwZO5diKA++B +99w== X-Gm-Message-State: AMke39mmABsMvNcSZO04MvccPOnLgciYAveVgvvquy9MS9WDgvqtbJA1uU6fK4eGGspzMA== X-Received: by 10.223.168.112 with SMTP id l103mr25491266wrc.184.1487861852535; Thu, 23 Feb 2017 06:57:32 -0800 (PST) Return-Path: Received: from [172.28.3.177] (ron.emn.fr. [193.54.76.162]) by smtp.gmail.com with ESMTPSA id o143sm6703202wmd.3.2017.02.23.06.57.30 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 23 Feb 2017 06:57:30 -0800 (PST) Subject: Re: [HoTT] about the HTS To: Vladimir Voevodsky , Univalent Mathematics , homotopytypetheory References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> From: Benedikt Ahrens X-Enigmail-Draft-Status: N1110 Message-ID: <484524d2-4054-5b7a-14af-e68a8e4b8375@gmail.com> Date: Thu, 23 Feb 2017 15:57:30 +0100 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:45.0) Gecko/20100101 Icedove/45.6.0 MIME-Version: 1.0 In-Reply-To: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit On 02/23/2017 03:47 PM, Vladimir Voevodsky wrote: > Just a thought… Can we devise a version of the HTS where exact > equality types are not available for the universes such that, even > with the exact equality, HTS would remain a univalent theory. > > Maybe only some types should be equipped with the exact equality and > this should be a special quality of types. > > Vladimir. > > PS If there are higher inductive types then the exact equality should > not be available for them either. Paolo Capriotti, in his PhD thesis "Models of Type Theory with Strict Equality" [1], has studied strict equality in type theory. >From page 69: "Finally, universes in the strict fragment of our system are not assumed to be fibrant types, like in HTS." You might be interested in Section 4.1.1, "Differences with HTS". [1] https://arxiv.org/abs/1702.04912