From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.4.33 with SMTP id v33mr2523328qtg.59.1513701702669; Tue, 19 Dec 2017 08:41:42 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.55.160.214 with SMTP id j205ls9496499qke.2.gmail; Tue, 19 Dec 2017 08:41:41 -0800 (PST) X-Received: by 10.55.200.218 with SMTP id t87mr2714080qkl.30.1513701701668; Tue, 19 Dec 2017 08:41:41 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513701701; cv=none; d=google.com; s=arc-20160816; b=Y479FBAWC28/QkXiVZsY4LjV+Pux8LYCS6OwmQRX3o6MXDpPkSSmkn5NhE6vXlDBhm xMZSmlLTINL92sEryNKag/PFi3jOyM3xoFYHdkhPgKps29KHQBUjlhjwRP8g03ZelYLD l3brShItLqMQArFMCy3KKbEX2R8xG6AREPDI0iU0HPD9v2k8zF2deLw1LS8+A/wSmNGA aHpCxHf8BR2czrmEG3S6t5XsSPnotq8wnz+iSPxn6oS+HL7shOiEQTKM2iH4KfUi1ja6 2VfzkI6uj0UNat2dSRD9hm9G+xQiCamf90zsf5Ks13X/Ql87SrBQZjpd44fLORDhetmg d+PA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature :arc-authentication-results; bh=BQN1tUwmlOTEe7+KEd+Kor2hgQ+OJoDdLwohiNwhFtI=; b=gZek3PaEDPpyxcOIIAu/w25pYR4SEjcr6wha44726NE1gLb3CL9IYjrYaNlxHPsQPq f3Fq1p5FSPMPSyyUjqlTqV1VrgjD1eBrMFRUgx2aHUpawUNAmKcGAjOOZH3eaUd/KvAZ xXOyrLgkUoUOSa0gFz2P2Cn12BX0lE4GpXzS8ZKEkeVi7ok8v4rJq0Fk5dxUWAJlP4Qn tD6CT9BGeTQUxOFdZ4DcqiqLUdsPOa8AkrMZe4RBj7LcerelS2KPitGvrj77NEYpxqq7 SOk4KRrUf3+CFBLROtu3eIRbruXqavVltlsFzL8QJBy0212Irn0h1XzlLA2Wd8HcUx3X x4mA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=PSfr/Xx1; spf=neutral (google.com: 2607:f8b0:400d:c0d::233 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-qt0-x233.google.com (mail-qt0-x233.google.com. [2607:f8b0:400d:c0d::233]) by gmr-mx.google.com with ESMTPS id c21si864449qkg.1.2017.12.19.08.41.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Dec 2017 08:41:41 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::233 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) client-ip=2607:f8b0:400d:c0d::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=PSfr/Xx1; spf=neutral (google.com: 2607:f8b0:400d:c0d::233 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-qt0-x233.google.com with SMTP id f2so24905586qtj.4 for ; Tue, 19 Dec 2017 08:41:41 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=BQN1tUwmlOTEe7+KEd+Kor2hgQ+OJoDdLwohiNwhFtI=; b=PSfr/Xx1W5ony8WS81Gzc4p3n5KeGxmIdYeADBd+OACbnUPj0dtFlHubTB6o9oAJDN gONloeVLLaK37/lqC9eHdug5Dr37J/dryFd052YyzD3kZlDi3Fd5NK/HnHLwfnlkiVOt OSb736lMUNBTdn/hWCoIR8KRHbkcWXoL6bW28W52Jsyv/+A+EefPqHNzMfeQh7fttxtW Hcw3kAVxFutduOS2H+1r+BzTtYsrtvhzCYhOdJz+11/scG0KGXhoxpt9GEsy3OnzcttK EbZvxz5iKwqZTxhxRABx1kz3T+9Ecq1X6gP/4M7LOvGPBiH+z6SOdia/fjqNhwjXEK1F 6iJA== X-Gm-Message-State: AKGB3mK3td3Y49Bh49A8OWVIcrGG5jRXKMgOvvrM57gD0lEC5eriR2At eLdiSduW7RtoXJzRF5gfVmfdXv1/KlU= X-Received: by 10.200.10.75 with SMTP id f11mr5373986qti.272.1513701701414; Tue, 19 Dec 2017 08:41:41 -0800 (PST) Return-Path: Received: from steveawodeysair.home (pool-74-98-210-201.pitbpa.fios.verizon.net. [74.98.210.201]) by smtp.gmail.com with ESMTPSA id v51sm9869570qtb.7.2017.12.19.08.41.40 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Dec 2017 08:41:40 -0800 (PST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 10.3 \(3273\)) Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? From: Steve Awodey In-Reply-To: Date: Tue, 19 Dec 2017 11:41:39 -0500 Cc: Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk> <20171212120233.GA32661@mathematik.tu-darmstadt.de> <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> <20171215170011.GA22027@mathematik.tu-darmstadt.de> <20171217102151.GA16619@mathematik.tu-darmstadt.de> <20171218115228.GB29410@mathematik.tu-darmstadt.de> <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk> To: Andrej Bauer X-Mailer: Apple Mail (2.3273) > On Dec 19, 2017, at 8:52 AM, Andrej Bauer wrote: >=20 >> I don=E2=80=99t understand this: HProps are subobjects of 1 hence they g= et classified as propositions. Hence there is an element of Omega correspon= ding to Sigle(a). >=20 > I beleive a lot of the confusion in this discussion would go away if > we translated some of what Thomas is saying into a more syntactic > setup. We have to be a bit careful about what "corresponds to" means. >=20 > To say that =CE=A9 classifies truth values, or h-propositions, means th= at: >=20 > 1. There is a type =CE=A9. >=20 > 2. There is a type family El(p) indexed by p : =CE=A9. >=20 > 3. For every p : =CE=A9 the type El(p) is an h-prop (there's a term witne= ssing this). >=20 > 4. For every h-prop P -- which is a type, not an element of =CE=A9! -- > there is p : =CE=A9 such that P is equivalent to El(p). (Again we need a > term witnessing the equivalence.) >=20 > Now, it may happen that h-props P and Q are both equivalent to El(r) > even though they are not equal. >=20 > Furthermore, there can be class-many subobjects of 1 in a topos, for > instance in sets there are class-many singletons. Of course, a whole > lot of them will be isomorphic and very many "correspond to" the > element =E2=8A=A4 : =CE=A9. But at least on this mailing list we're not i= n the > business of sweeping isomorphisms under the rug. So far so good, but the last remark is a bit too cryptic. If this is supposed to be subobject classification in the sense of an eleme= ntary topos,=20 then the p=E2=80=99s that =E2=80=9Ccorrespond to" isomorphic h-props still = need to be identified. That=E2=80=99s univalence for Omega, of course, which does indeed hold in a= topos. Otherwise, you are talking about a looser notion of =E2=80=9Cclassification= =E2=80=9D of h-props. Steve >=20 > With kind regards, >=20 > Andrej >=20 > --=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= email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.