From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.156.216 with SMTP id t207mr11366242ywg.166.1487861277624; Thu, 23 Feb 2017 06:47:57 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.69.193 with SMTP id c62ls1136473itd.17.gmail; Thu, 23 Feb 2017 06:47:56 -0800 (PST) X-Received: by 10.99.234.5 with SMTP id c5mr11783544pgi.172.1487861276834; Thu, 23 Feb 2017 06:47:56 -0800 (PST) Return-Path: Received: from pps5.ias.edu (pps5.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id r198si435646ywe.4.2017.02.23.06.47.56 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 23 Feb 2017 06:47:56 -0800 (PST) Received-SPF: pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) client-ip=192.16.204.88; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) smtp.mailfrom=vlad...@ias.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=ias.edu Received: from pps.reinject (pps5.ias.edu [127.0.0.1]) by pps5.ias.edu (8.16.0.17/8.16.0.17) with ESMTPS id v1NEluHX007825 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Thu, 23 Feb 2017 09:47:56 -0500 Received: from pps5.ias.edu (pps5.ias.edu [127.0.0.1]) by pps.reinject (8.16.0.16/8.16.0.16) with SMTP id v1NEluOk007817; Thu, 23 Feb 2017 09:47:56 -0500 X-Proofpoint-Sentinel: stfjJm+FJaMIML7wSL4Iq6H5y/b+z9CI91p/zPPs2D+qHQtTYWx0ZWRfXz98 sca0w5tsmphxJlQVyxicAQQWqzSIvCOaVpz1G+hpzoe4/fy0ZlIK9geQl1VGyQTR9tQXNdqanHkm 0LCmhVVkKFyu9tlAPg== Received: from imap.math.ias.edu (f5-bip.net.ias.edu [172.16.13.241]) by pps5.ias.edu with ESMTP id v1NEluxS007816 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Thu, 23 Feb 2017 09:47:56 -0500 Received: from pool-96-248-86-80.cmdnnj.fios.verizon.net ([96.248.86.80] helo=vladimirs-mbp-2.home) by imap.math.ias.edu with esmtpsa (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.80.1) (envelope-from ) id 1cgugV-0002nL-VQ; Thu, 23 Feb 2017 09:47:55 -0500 From: Vladimir Voevodsky Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 10.2 \(3259\)) Subject: about the HTS Message-Id: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> Date: Thu, 23 Feb 2017 09:47:55 -0500 Cc: "Prof. Vladimir Voevodsky" To: Univalent Mathematics , homotopytypetheory X-Mailer: Apple Mail (2.3259) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-02-23_11:,, signatures=0 X-Proofpoint-Spam-Reason: safe X-IAS-PPS-SPAM: NO X-Proofpoint-Spam-Details: rule=ias_safe policy=ias score=0 spamscore=0 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=donotscan adjust=0 reason=safe scancount=1 engine=8.0.1-1612050000 definitions=main-1702230138 X-IAS-PPS-PHISH: NO Just a thought=E2=80=A6 Can we devise a version of the HTS where exact equa= lity types are not available for the universes such that, even with the exa= ct equality, HTS would remain a univalent theory. Maybe only some types should be equipped with the exact equality and this s= hould be a special quality of types. Vladimir. PS If there are higher inductive types then the exact equality should not b= e available for them either.=20