From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.40.80 with SMTP id o77mr167067ioo.39.1513614322893; Mon, 18 Dec 2017 08:25:22 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.128.194 with SMTP id k63ls2491337ioi.20.gmail; Mon, 18 Dec 2017 08:25:21 -0800 (PST) X-Received: by 10.107.128.203 with SMTP id k72mr154738ioi.127.1513614321954; Mon, 18 Dec 2017 08:25:21 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513614321; cv=none; d=google.com; s=arc-20160816; b=L3QHXR1E0b0B/Nfwl0eRcuc2Nlmjcu9Dpq1vpE/Nl/LAqM+hMPBuJ3a/oGVj1ltO1c 7Ymlg4sIG5pbBounP2qM7murnGKbrgIP3AKCkgYLlIGjpvpv9XKPoiQUrCc9WCPzeAzo 6UGgpk6ioGmehvQ6IoSH/E17kUeMkbPKVPA0ahdGYWllYmFFDV8gSvytJqw9OPM+mRgi SZntguCxodMaBINj/L6nivNZOG9bVQXiMIVfW6Kf+JDMTX0DWUrcBwi2abXbbmG3w7K4 0jEbUMNRiI/nRwiRB/MbZ7Weo0n5FfDGlP+FagUz60pXUYOZLzR9X0qeGng3nGHb3lYg 2dhA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=VFNyTz5JukQnDMMbNS6THPCEeYrFmZjBmvFHKpiyumk=; b=dvo7fA5sTZBoa4vU3JtZewtvThUy0/cffMoSg+T1gGNTcv6rqkDhG/UoOZOmL+qWsr kS+iw+yxFnwxvQ3lbdNvpyh63VY4lhpk6OF65MOCVPtmndWjDJxM2w3hutdWAnE56rdV DzOC8AsL1Xx1YsyWMA9rNqy7vhX+3c1bZ2Amk4Rbo7SBTWizp7TgShpNzKuEOAA2dYkY iVJBhpIS3+VI//TWYOlj2T2VVnvGrglg3mlRs8g87yhBpA5SuU4+lh6Rpe0m/QOWuz8D qW4pZ6SGhsw6o4YH0f7oBwWsxnUPFSNM2m07j1pocTavonv4vg8b+HC8jf9ELpjlb2XV 6dyQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=q0pQWAoX; spf=neutral (google.com: 2607:f8b0:4003:c0f::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-ot0-x234.google.com (mail-ot0-x234.google.com. [2607:f8b0:4003:c0f::234]) by gmr-mx.google.com with ESMTPS id x189si936276ite.2.2017.12.18.08.25.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Dec 2017 08:25:21 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4003:c0f::234 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4003:c0f::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=q0pQWAoX; spf=neutral (google.com: 2607:f8b0:4003:c0f::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-ot0-x234.google.com with SMTP id y10so13800085otg.10 for ; Mon, 18 Dec 2017 08:25:21 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=VFNyTz5JukQnDMMbNS6THPCEeYrFmZjBmvFHKpiyumk=; b=q0pQWAoXlqmeHHpGr1N3fsd3+1rbX6nPnkYdUCWexirlvxhi3wgy2cHf9Tp09x7Mrd jBcWG4U+CREM/3CKBy0gHkOAaCnQ+V48QBG9sUUmlUxbNmg+O6XUvV7NLYYAfIThiRV3 H9kxlWsZ1GrN58b3b2/MnCvZDNduB/bkt7rh3hHa+gp+fAnuXsbE7gME7hcjrVbNyTBZ U4vEMFLovYXQ63FZgp6zTrcRNC4KCz2fQFYF1zWbPPTi2pCwE+V0z5NTdKK/JNZ7zf6J hyagZvO9e9njvTc2bo3ySeeBDnXoOedqZShLXu4Y92KZfj8Ksg9m/sCe/hi3ROja+2z8 ftew== X-Gm-Message-State: AKGB3mKriif1RMDe/b+JJh4x+FTHxgPZ7ABWFOIIlcF4QQRAKFimKxhc sbqGeZbYtG/UzzgVC4FJ+vXvSs07eKM= X-Received: by 10.157.92.197 with SMTP id r5mr119444oti.286.1513614321359; Mon, 18 Dec 2017 08:25:21 -0800 (PST) Return-Path: Received: from mail-ot0-f176.google.com (mail-ot0-f176.google.com. [74.125.82.176]) by smtp.gmail.com with ESMTPSA id h138sm5764453oib.16.2017.12.18.08.25.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Dec 2017 08:25:20 -0800 (PST) Received: by mail-ot0-f176.google.com with SMTP id q39so7381569otb.8 for ; Mon, 18 Dec 2017 08:25:20 -0800 (PST) X-Received: by 10.157.9.153 with SMTP id q25mr101731otd.131.1513614320425; Mon, 18 Dec 2017 08:25:20 -0800 (PST) MIME-Version: 1.0 Received: by 10.157.6.228 with HTTP; Mon, 18 Dec 2017 08:24:59 -0800 (PST) In-Reply-To: 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> From: Michael Shulman Date: Mon, 18 Dec 2017 08:24:59 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" HITs involve equality, so if equality is a static prop, then it is involved. On Mon, Dec 18, 2017 at 3:55 AM, Matt Oliveri wrote: > Oh right. Static propositions alone doesn't seem to guarantee a quasitopos > either. > > I thought HITs make sense with static props. After all, the type of > propositions isn't even involved, formally. > > On Monday, December 18, 2017 at 5:00:51 AM UTC-5, Michael Shulman wrote: >> >> That seems about right to me, except that I don't know whether a >> static universe of props without unique choice *actually* gives a >> quasitopos. It gives you a class of subobjects that have a classifer, >> which looks kind of like a quasitopos, but can we prove that they are >> actually the strong/regular monos as in a quasitopos? And a >> quasitopos also has finite colimits; do HITs make sense with a static >> Prop? >> >> On Sun, Dec 17, 2017 at 11:41 PM, Matt Oliveri wrote: >> > Hello. I'd like to see if I have the situation straight: >> > >> > For presenting a topos as a type system, there are expected to be (at >> > least) >> > two styles: having a type of "static" propositions, or using hprops. >> > >> > With hprops, you can prove unique choice, so it's always topos-like >> > (pretopos?). >> > >> > With static props, you can't prove unique choice, but it may be >> > consistent >> > as an additional primitive, or you can ensure in some other way that you >> > have a subobject classifier. >> > >> > If you don't necessarily have unique choice or equivalent, you're >> > dealing >> > with a quasitopos, which is a more general thing. >> > >> > With static props and unique choice, subsingletons generally aren't >> > already >> > propositions, but they all correspond to a proposition stating that the >> > subsingleton is inhabited. Unique choice obtains the element of a >> > subsingleton known to be inhabited. >> > >> > The usual way to present a topos as a type system is with a >> > non-dependent >> > type system like IHOL. This will not be able to express hprops, so >> > static >> > props is the way. Proofs will not be objects, so proof-irrelevance >> > doesn't >> > come up. >> > >> > The static props approach can also be used in a dependent type system, >> > along >> > with unique choice or equivalent. (To say nothing of whether that's a >> > natural kind of system.) >> > >> > In a dependent type system, a type of static props may or may not be a >> > universe. >> > >> > If it's not, proofs still aren't objects and proof-irrelevance still >> > doesn't >> > come up. >> > >> > But if it is, you should at least have typal proof-irrelevance. (That >> > is, >> > stated using equality types.) >> > >> > In that case, with equality reflection, you automatically get judgmental >> > proof-irrelevance. This does not necessarily mean that proofs are >> > computationally irrelevant. With unique choice, they cannot be, or else >> > you >> > lose canonicity. >> > >> > All OK? > > -- > 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.