From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.55.215.85 with SMTP id m82mr2274693qki.15.1513691558042; Tue, 19 Dec 2017 05:52:38 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.233.237.87 with SMTP id c84ls9266921qkg.5.gmail; Tue, 19 Dec 2017 05:52:36 -0800 (PST) X-Received: by 10.55.152.197 with SMTP id a188mr2332273qke.31.1513691556552; Tue, 19 Dec 2017 05:52:36 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513691556; cv=none; d=google.com; s=arc-20160816; b=gSg1dfL0HnKQhjvGdj19oCp7gJHVH1pKMu1uHZWFsnMjaFbmO9mS9YHtaIUxkqOHwy TUtWOoY32RcRspTns6qJpNUPtDWI+YLUwx4PqpdDFSSvJYccL8JReJ8OMuDV7FcEzfHb xINKFqy0NfzD0PcwDSX3gvGFUIu9/BvTviOzGYzrikKrQl0Oz34O7LbTgRBjxH1VeChG WXUPt8nK+VNdhedElKf+YADqTCXUeVs0Ohne/PRjpn+o0QO5CNJCNlnlYDhh8y2fluKK O23kzXL8n0dYvlw4gxSSYuZD1apnsTtk3+p1fDLlRpyZzjM4DAt+r8vDIwwlzQQfQwaS 33FA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=vK29mRamkPCnBT5dUIdtrYaKm5hkPAIdkDHt/EoUwas=; b=IdczsIONvRWO799LwBQXVyKtq5hfZn++lBX11GeYXrK2X9CCJFNHwEJbCyqn35C5Yn gFp57MTx6ILQPF9Wz0zQ3r7hZL0dpuhHaY74k9EGSyPYTWbvpYS1XtVwR9UjhEvyzsuq KFzqQiA851MWfF07aU+xSa7Qukq0aVX/cSGbk8u3rTOY2rtozW4w4RHeia01Cx6YGRvc CigABqCFbNDQMg91yEI5g9UPkc/mmc5oIgYuQ/KZNdnQO2Je1FlAcGp+oouW9rXM6rei 9BVgVDH5Bu8qnBtHar3P7U5om48+SgdTViN+3pKJjDQ+oSNnkl3OLn8QOfA9BD/TUsFr Zh8Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=k1+iWpix; spf=neutral (google.com: 2607:f8b0:4002:c09::22a is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Return-Path: Received: from mail-yb0-x22a.google.com (mail-yb0-x22a.google.com. [2607:f8b0:4002:c09::22a]) by gmr-mx.google.com with ESMTPS id m11si846726qth.0.2017.12.19.05.52.36 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Dec 2017 05:52:36 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22a is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4002:c09::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=k1+iWpix; spf=neutral (google.com: 2607:f8b0:4002:c09::22a is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-yb0-x22a.google.com with SMTP id j7so13644534ybl.3 for ; Tue, 19 Dec 2017 05:52:36 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :content-transfer-encoding; bh=vK29mRamkPCnBT5dUIdtrYaKm5hkPAIdkDHt/EoUwas=; b=k1+iWpixR9j4m4nVEdSwRbrU42XUbAu6dtU/LI8JPWs82GC7AAfc9BixEr4cKz+XWB hbq0aAOQwV24wtR5ybcEQTVKGqojoEJ3onfky3bKRIvROuA0fy/7YTtTlo3c8X63gH0P BMTFs0fSLewvwElln3BkU4Zfru+TiJNjZ2XqDlMrxoCgrarDv+jNeHc4JRfMYsigryfU JJlDw4ZkBCBBZC3C4CEy5aB41mu7iqZZ1rq5O2ZUgFwHFc/s1Bn8CuJlHIk7AflFVjgz TyUbmOTrpbqYLY9nc1Qm+vkBkQbV70hkRn8uJJZNsumngdvQNG0kVfLAmokD7T0AMgNG FOWQ== X-Gm-Message-State: AKGB3mId4PZeSKr0Ar8C5XxZfXOOa44ok0sTc9OlL/DiIwXvCCK33+aH VL7bvcu189GP9kL3WdYybPLqpww/UvmpZkHCEmMm4dS/ X-Received: by 10.129.112.1 with SMTP id l1mr2304260ywc.389.1513691555910; Tue, 19 Dec 2017 05:52:35 -0800 (PST) MIME-Version: 1.0 Received: by 10.37.9.2 with HTTP; Tue, 19 Dec 2017 05:52:35 -0800 (PST) X-Originating-IP: [95.159.200.250] In-Reply-To: <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk> 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> From: Andrej Bauer Date: Tue, 19 Dec 2017 14:52:35 +0100 Message-ID: Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > I don=E2=80=99t understand this: HProps are subobjects of 1 hence they ge= t classified as propositions. Hence there is an element of Omega correspond= ing to Sigle(a). 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. To say that =CE=A9 classifies truth values, or h-propositions, means that= : 1. There is a type =CE=A9. 2. There is a type family El(p) indexed by p : =CE=A9. 3. For every p : =CE=A9 the type El(p) is an h-prop (there's a term witness= ing this). 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.) Now, it may happen that h-props P and Q are both equivalent to El(r) even though they are not equal. 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 in = the business of sweeping isomorphisms under the rug. With kind regards, Andrej