From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.0.147 with SMTP id e19mr3954172lji.6.1487875977815; Thu, 23 Feb 2017 10:52:57 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.20.28 with SMTP id u28ls166197ljd.10.gmail; Thu, 23 Feb 2017 10:52:56 -0800 (PST) X-Received: by 10.25.213.11 with SMTP id m11mr4161506lfg.19.1487875976737; Thu, 23 Feb 2017 10:52:56 -0800 (PST) Return-Path: Received: from mail-wm0-x236.google.com (mail-wm0-x236.google.com. [2a00:1450:400c:c09::236]) by gmr-mx.google.com with ESMTPS id f7si551116wmg.3.2017.02.23.10.52.56 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 23 Feb 2017 10:52:56 -0800 (PST) Received-SPF: pass (google.com: domain of benedik...@gmail.com designates 2a00:1450:400c:c09::236 as permitted sender) client-ip=2a00:1450:400c:c09::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of benedik...@gmail.com designates 2a00:1450:400c:c09::236 as permitted sender) smtp.mailfrom=benedik...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x236.google.com with SMTP id v186so180434984wmd.0; Thu, 23 Feb 2017 10:52:56 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:cc:from:message-id:date:user-agent :mime-version:in-reply-to:content-transfer-encoding; bh=tzqmuJtcmKQBSTt/K4aVzQErrzEgNABIh6opWZ1wDEM=; b=PVMEwXuxIuTs7RiDB/MhBWHDtpFtfjWDdA8aSiJFyMnfuKDQG+InMCJgd+AdF3xIrt ugkj4wXZksGI9bq2/oMmWvUtnKECeSxjj//23HvItw8jiEKUXp8lUj6M3fbMhRgUjqDF dse5qiebL5uNZp4ytngszSCgZ/wAjT18H4OvTgY2k63F1JeKEHFK+5mhf57e7ljQWWIh /ocsBETMEf81xJqsvuYNNTY9Dj7w6BANdncQ5r2QMJ/wkrhY3qEkW7+2ffpWy8Ea2zVp gNLJ9fXbAV8/HpwCWRhL728d7ZtyF+zW1aIlJ4ypCPf9/U1PDcLsO9tCRzudrcW6OU+B G6Ug== X-Gm-Message-State: AMke39k8JlkMXkcH0iiMR/DnJtSXcxzLgVGiAVdKzh5dPg9gIHfouhY7xJfZtsJgww3lDg== X-Received: by 10.28.156.86 with SMTP id f83mr5872667wme.93.1487875976313; Thu, 23 Feb 2017 10:52:56 -0800 (PST) Return-Path: Received: from ?IPv6:2a01:cb05:891c:2d00:6680:99ff:feed:97f7? (2a01cb05891c2d00668099fffeed97f7.ipv6.abo.wanadoo.fr. [2a01:cb05:891c:2d00:6680:99ff:feed:97f7]) by smtp.gmail.com with ESMTPSA id 191sm7475154wmo.21.2017.02.23.10.52.55 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 23 Feb 2017 10:52:55 -0800 (PST) Subject: Re: [HoTT] about the HTS To: Vladimir Voevodsky References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> <484524d2-4054-5b7a-14af-e68a8e4b8375@gmail.com> <91160F61-2A67-4B1F-9A4A-F3510B99E9D3@ias.edu> Cc: Univalent Mathematics , Paolo Capriotti , homotopytypetheory From: Benedikt Ahrens Message-ID: <29b2bdf5-3838-a268-5a44-4aea998cb878@gmail.com> Date: Thu, 23 Feb 2017 19:52:54 +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: <91160F61-2A67-4B1F-9A4A-F3510B99E9D3@ias.edu> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Section 1.4.8 "Equality" gives an informal account and points to several precise definitions. On page 43 two equality types are considered, one intensional one and one with reflection rule. Maybe Paolo (in CC) can explain his setup himself. On 02/23/2017 07:08 PM, Vladimir Voevodsky wrote: > I could not find where he defines the univalent (intensional) > equality. It seems that all his equalities are strict. > > >> On Feb 23, 2017, at 9:57 AM, Benedikt Ahrens >> wrote: >> >> >> >> 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 >> >> -- 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 >> HomotopyTypeThe...@googlegroups.com. For more options, >> visit https://groups.google.com/d/optout. >