From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a5b:aca:: with SMTP id a10-v6mr9786097ybr.31.1525533234238; Sat, 05 May 2018 08:13:54 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:a881:: with SMTP id f123-v6ls984313ywh.2.gmail; Sat, 05 May 2018 08:13:53 -0700 (PDT) X-Received: by 2002:a0d:f601:: with SMTP id g1-v6mr1660870ywf.123.1525533233317; Sat, 05 May 2018 08:13:53 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525533233; cv=none; d=google.com; s=arc-20160816; b=L4IM7CFfSd6hdMl0ZGAHpRYoZyDr9KLAtXd4QR8p2A1C8HzyVqEwzdM74u79bBEjp0 Pw5mO+rbxCoTXWpHxZx4LkDpujUTOfAW/WehIbwmm6RSZ+wWhsczLd9hXaWl1Tli6frL P1IgbIqatNfrRRVf/hyIQq2U57UUL6FOJIzUJ++6xe2gm3QkLCEdwnKDOmNGB7lxFUFc Zpm97KE2wcjyGKbW6F9AJzBTPhWxWcKvE0OI2y5WlFTXyUqrwPnlX1qxb3tSF2vC0tZa KeJNAyomFy1hcRUdJhdf2bmShcFjPSRrddDDvDDBxoT8b8hVRbcN5AZfHcwYVkUc1W1I lVkQ== 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=a8E3vm4gG0m/nPO465xmkeFKb1NZPmYOb1PPOgHYwT4=; b=g06edtAZ413ex1WfIY2qWcSxTkup1jupLcMqPjz2VytWuKywqs0UV779exF1/05XHW YDjXyGK7RfstEh7gYnBVxptPDsDwFx9TQk7zbooOZSEiu4npgGzzsMPALFruh3Io79yX h3FPR3ytXic/FG2RPvB+nOl7ZkJ1GftuAtiAmuXUP+/Ua56+BJDlSjuKfp7w0H1ivacc kOz+3tJcWoy6CVtCNYQTCNtvc2e1JO3sYMMM7TwjHPfmTDV2wpBg6dh3NBnxgt42NZKJ FvqN2/QLMOWVVKWgULNbAuMDo321VkgPgl7h098Sts8ZVbAHckaiiCZ0XJnJzXClC6hS +lxQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=bcI9Re4X; spf=neutral (google.com: 2607:f8b0:4002:c09::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x230.google.com (mail-yb0-x230.google.com. [2607:f8b0:4002:c09::230]) by gmr-mx.google.com with ESMTPS id o63-v6si1193436ybc.2.2018.05.05.08.13.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 05 May 2018 08:13:53 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::230 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=bcI9Re4X; spf=neutral (google.com: 2607:f8b0:4002:c09::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x230.google.com with SMTP id r13-v6so8629580ybm.12 for ; Sat, 05 May 2018 08:13:53 -0700 (PDT) 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=a8E3vm4gG0m/nPO465xmkeFKb1NZPmYOb1PPOgHYwT4=; b=bcI9Re4XOBNozNbHoqrXhucDCqJWtBYw3lhnsci2KtHHXEuicu9jyagrXQjFmfBhtf XgEICTeybdz6d1V/iSVRbtw+Ma98XFmeGot0nu93Krtb8M2j5yc3eNu+eLNT3v03TAsR tz+RBqBtdqY5Iscjk5kRCfBIopEbtgNWvGq9ODF6HmoKo0M+921SvTUBiW4Z6m+6wZMz 1h8xrPovw7wykC3BAYtI5jwf+VhO1ycD+8NK3fxW4c+aoP4peqIsS432d0R9Sf8MXdxB C31mWuTR+2zMHJGKJsw507jcIxcjHLmmycN3sA4iPKepc/t+dS3VUXBFSPCi+UOZurDB TOQQ== X-Gm-Message-State: ALQs6tAR+OWgjlA1OtEaaT3b4pV1c5GgcLZokKHBrz0TKFdz2KcWWKEo naMYKjO6F49m8qv2JgefaI0Q3Fd8 X-Received: by 2002:a25:b2a4:: with SMTP id k36-v6mr19172440ybj.259.1525533232769; Sat, 05 May 2018 08:13:52 -0700 (PDT) Return-Path: Received: from mail-yb0-f178.google.com (mail-yb0-f178.google.com. [209.85.213.178]) by smtp.gmail.com with ESMTPSA id r207-v6sm8752868ywg.23.2018.05.05.08.13.51 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 05 May 2018 08:13:52 -0700 (PDT) Received: by mail-yb0-f178.google.com with SMTP id y5-v6so8644518ybg.0 for ; Sat, 05 May 2018 08:13:51 -0700 (PDT) X-Received: by 2002:a25:7c03:: with SMTP id x3-v6mr19801015ybc.120.1525533231623; Sat, 05 May 2018 08:13:51 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d297:0:0:0:0:0 with HTTP; Sat, 5 May 2018 08:13:50 -0700 (PDT) In-Reply-To: References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> <32baa760-53ed-4fa4-b69c-9537be5b63aa@googlegroups.com> <385f5d47-0656-4a4d-b24c-c2abeab629e7@googlegroups.com> From: Michael Shulman Date: Sat, 5 May 2018 08:13:50 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Bishop's work on type theory To: Thorsten Altenkirch Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" I think the problem is that it's not consistent about what a "proposition" is. If a "proposition" is a setoid in which all elements are equal, then to be consistent, the equality relations of other setoids should also be valued in "propositions" of *this* sort, not the original collection of "propositions" you started with. Otherwise, I think you won't necessarily be able to take the quotient of a setoid by a "proposition"-valued equivalence relation, which is the whole point of introducing setoids in the first place. But down this route lies infinity. I only know of three ways to get a well-behaved category of setoids: 1. Use propositions as types, as in MLTT Type-valued setoids and the ex/lex completion. 2. Define a morphism of setoids to be not an operation respecting equality but a total functional relation, as in the tripos-to-topos construction and the ex/reg completion. I personally believe this is the correct solution in the most generality, but Bishop-style constructivists don't seem to like it. 3. Assume the axiom of choice, which causes options (1) and (2) to coincide. On 5/5/18, Thorsten Altenkirch wrote: > > > On 05/05/2018, 05:27, "homotopyt...@googlegroups.com on behalf of > Michael Shulman" shu...@sandiego.edu> wrote: > >>3. He includes the axiom of choice (p12) formulated in terms of his >>(proof-irrelevant) propositions, as well as what seems to be a Hilbert >>choice operator (though it's not clear to me whether this applies in >>open contexts or not). Since he has powerclasses with propositional >>extensionality, I think this means that Diaconescu's argument proves >>LEM, which he obviously wouldn't want. It's harder for me to guess >>how this should be fixed, since without some kind of AC, setoids don't >>satisfy the principle of unique choice. > > Why not? If we identify propositions with setoids that are internally > propositions (all elements are equal) and identify propositions upto > logical equality we get unique choice. > > What do I miss here? > Thorsten > > >> > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > >