From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.176.80.46 with SMTP id b43mr2617706uaa.41.1513742111966; Tue, 19 Dec 2017 19:55:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.176.2.9 with SMTP id 9ls5796834uas.14.gmail; Tue, 19 Dec 2017 19:55:10 -0800 (PST) X-Received: by 10.31.154.148 with SMTP id c142mr2348300vke.59.1513742110884; Tue, 19 Dec 2017 19:55:10 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513742110; cv=none; d=google.com; s=arc-20160816; b=gZG9FUOkKsHPnlHr7siLeqV2tcdY1/dhjtx5RwC08xMnMP54U64Xr/EN8UMlDrbThK pZx9qSaGVGkjiydrQA4HFOnFNJMiRozzkM6cZ3Hb8ZBAP//0wHBv2VMSowa8CpnicwSK pdjmXgl7UZJ1WzGrA/jRHyQwFr9/+px8cJxzgfpCFj5ASB7BIU3fitoe+1+ujBLIZw3J vD2ez7nKnQ+ML1vB5Xy5tF6ME4YoThfGiV+/s/9RCk+p/yPa2oBcVqmbRZiCsCa1kn4Y 68wYsn1qEHUJm3EQu+KO/Br2WofUgmqhBoWmc0I/0C9WmujV+8xTfnwv66rJVd9o4O0s 0/rw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=message-id:in-reply-to:to:references:date:subject:mime-version :content-transfer-encoding:from:dkim-signature :arc-authentication-results; bh=yhXFVh5DIdCxXJDEusdaXD4Oblxq1g5cHSoND3+BlEw=; b=K/lUyTZ7kI1qj94k/G5xRqmgpER8MrIaumQCEv6Gfq2NEVJZLVE17pmdwMskEyfjXn fGqeRUpHFy+8QEy/ifawv1Z4qNubjjn74W8xLb9dDw0mnz4xvWvq1QYSXNyB4U/E16h/ YOiaZ5r28RB8aKpjXT9x42y9ABRRfuTNt+feJMSLUAvlUUeW3ec0rR3t9VkEzgOiIdu4 V341g6FKIJAQflwZzV5aRce2uAjBFlLAljzkMQU3gZYI2i7haVGXbHpvNEdgaZhFrxRe ZG//kEIqALmjba+RzfUrdvCRluTYBTyVJtfA/xDIMC0iiJRZcGc2lM2UOyCi/NtFHZl8 shSg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=qTIWdBkI; spf=neutral (google.com: 2607:f8b0:400d:c0d::229 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-x229.google.com (mail-qt0-x229.google.com. [2607:f8b0:400d:c0d::229]) by gmr-mx.google.com with ESMTPS id v125si495269vkg.5.2017.12.19.19.55.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Dec 2017 19:55:10 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::229 is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) client-ip=2607:f8b0:400d:c0d::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=qTIWdBkI; spf=neutral (google.com: 2607:f8b0:400d:c0d::229 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-x229.google.com with SMTP id w10so26781401qtb.10 for ; Tue, 19 Dec 2017 19:55:10 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=from:content-transfer-encoding:mime-version:subject:date:references :to:in-reply-to:message-id; bh=yhXFVh5DIdCxXJDEusdaXD4Oblxq1g5cHSoND3+BlEw=; b=qTIWdBkIBNbrGywS99Q5MxFBfl3GratqLXDb7G2xN/TGOchIfUz+D9FlhsYk29LpbT S6CRoxo28y1FFz1BQaJmmCA9ICmqVVnBWEc0w4waUysVmlWKRYNOD33/4T7xeoP2AKdE cruIyV+QxU1RCR5Oh9sD9BzRs6cb4z1fMZzGqIFwr0s1lk7WOYd/R5jdEwO1IAoY24Tp NUzxH12HSdpR0CRnCvDXhaWofcQnAGGkb+ICyTKcQbnRmtq7YcWvr7/tITnAAu9+ywkk NPWbiRnTzbuST1XEx3+PpfUVyzBXNOv9cOYbyPV0L7pekOBRYz7E/Ss3OE2578SQ/P3C KHTg== X-Gm-Message-State: AKGB3mIoSNOa/qNdiwNvhj3w6MfZsz/TTt2SPe73h0tJcvMIdrEySMjF z3LD/cFI6iPTEyZhEMZFiBgnVt7CpLQ= X-Received: by 10.200.25.134 with SMTP id u6mr7731291qtj.221.1513742110483; Tue, 19 Dec 2017 19:55:10 -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 y23sm10576674qtj.24.2017.12.19.19.55.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Dec 2017 19:55:09 -0800 (PST) From: Steve Awodey Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 10.3 \(3273\)) Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Date: Tue, 19 Dec 2017 22:55:09 -0500 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: Homotopy Type Theory In-Reply-To: Message-Id: X-Mailer: Apple Mail (2.3273) Yes, that=E2=80=99s fine, but it wasn=E2=80=99t part of your reformulation = (at least not explicitly).=20 Steve Sent from mobile - sorry fr typos. On Dec 19, 2017, at 19:14, Andrej Bauer wrote: >> If this is supposed to be subobject classification in the sense of an el= ementary topos, >> then the p=E2=80=99s that =E2=80=9Ccorrespond to" isomorphic h-props sti= ll need to be identified. >> That=E2=80=99s univalence for Omega, of course, which does indeed hold i= n a topos. >=20 > Isn't Thomas's point that the p's that correspond to isomorphic > h-props are *equal*, and that there is only one reasonable notion of > equality in a topos, which is extensional equality? >=20 > With kind regards, >=20 > Andrej