From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.55.154.212 with SMTP id c203mr19541044qke.0.1525533677405; Sat, 05 May 2018 08:21:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:f643:: with SMTP id s3-v6ls5038132qvm.6.gmail; Sat, 05 May 2018 08:21:16 -0700 (PDT) X-Received: by 2002:a0c:89b3:: with SMTP id 48-v6mr18743517qvr.22.1525533676648; Sat, 05 May 2018 08:21:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525533676; cv=none; d=google.com; s=arc-20160816; b=deuzyymWrngLrp9euFM2E2Ik3lXJ6W+0OKFOJLsIik/QCtID8PDq2RbiW9KySBHDIQ JLpTIZUzlYVWoToRJJfSvCMsW7EMC/JSroEv3/hko4j7NyG/QqxZU8A88xbRmBiGGEz6 7j9ItE7Nv378+tAERp6Pc0wVZEoi5viPgA/4tgGEKGJfudpLlBaPHMerbnFoGBRa1xWV NariejZ//VKPFHMIXMsngUjlYbyXP9q6fwcmF3wby4H0oHVr+slAwUaPjpW94J/sHq5n R4P+lPEtv55LSrFCbVlLF3jLUrakfULPhPtAIL4AY4aRYeH34GfYAUrrR4nNzKAqZ/KO RUEA== 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=F/Y/IbZjRlrTqXgS1svVYZPhNR0ovGpqbwPd7DQescI=; b=RzAvmcIkF2YsFF/AifqYp0JECjSmHfN2dIo+zL/JVzMM+5tAgfD7xsZlGOE9H3kt9N 91XkLNeQIdYLp2Tdf4bdMV64JEMvA5QaHtXB0EKJv0lcsFaTlbpLFOP8yUJNG01NLeeN kLQrfP/ZAOwup9dkv3F+QpHDeuCgqlwKKsZIgwLfX9yrbsT4xFCqoBzk3oaTz3xeTuor 15uMGiKoeRZZnHVkJziCQWpAsxQXLKBhu1c2oamVHYl+UeuVpGMVO7gAg9iePFSKtHie bQl7tzEdHhflxVism3G2S7dbiwL/2QV4QJQunN5/AUkxhHTc4uibg+EB3qFiQVj9ZRdH Y3kA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=NBKraLp6; spf=neutral (google.com: 2607:f8b0:4002:c05::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x236.google.com (mail-yw0-x236.google.com. [2607:f8b0:4002:c05::236]) by gmr-mx.google.com with ESMTPS id m7-v6si902126qtg.2.2018.05.05.08.21.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 05 May 2018 08:21:16 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::236 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=NBKraLp6; spf=neutral (google.com: 2607:f8b0:4002:c05::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x236.google.com with SMTP id p144-v6so7510903ywg.7 for ; Sat, 05 May 2018 08:21:16 -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=F/Y/IbZjRlrTqXgS1svVYZPhNR0ovGpqbwPd7DQescI=; b=NBKraLp6hBVbha0/CmZBve7b7N96q6tDgdLSBjGB12LzLBLU1TtpIPHNTsyt5Bu4l0 /4dM0ImUQcpz6hCCs8soaHo5HwlP6JswEf8qqbv9wVYOxkvDkp0wHTgSfF+lesNRe6yk ut3fKCc3x4jhQcadanF7Otnagu0roQxUpj2CJXawcHvVzZ8DTeqIhXvs123MViaCnbqq CugspAN+l85zt3AqG0h10qT4HKPLo/Hef19KKLoN1WS0GwG2sDU1eyqtw6rhmmT2LvCg GVoxYX8DxSq/vEOrcibrJSK1XrE9Qag1OhXS4Awr+FCTaPoPfzKqOMALS8f3OLsO0gok kEKg== X-Gm-Message-State: ALQs6tA1tTdWRcplEc54QSQgz+/dOpdmGRmbnRJzveV515kqDpbdBWPD Dsm7zqR5RfUFIByLxL8zbNhB8CC+ X-Received: by 2002:a81:7757:: with SMTP id s84-v6mr17543095ywc.17.1525533675969; Sat, 05 May 2018 08:21:15 -0700 (PDT) Return-Path: Received: from mail-yw0-f182.google.com (mail-yw0-f182.google.com. [209.85.161.182]) by smtp.gmail.com with ESMTPSA id c3-v6sm204687ywh.105.2018.05.05.08.21.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 05 May 2018 08:21:15 -0700 (PDT) Received: by mail-yw0-f182.google.com with SMTP id g9-v6so7508638ywb.12 for ; Sat, 05 May 2018 08:21:15 -0700 (PDT) X-Received: by 2002:a81:8004:: with SMTP id q4-v6mr4627721ywf.246.1525533675343; Sat, 05 May 2018 08:21:15 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d297:0:0:0:0:0 with HTTP; Sat, 5 May 2018 08:21:14 -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:21:14 -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" Of course, if you have higher-order logic with propositional extensionality, you don't need to use setoids at all, but can instead define quotients as sets of equivalence classes like in ZF. But I suspect Bishop wouldn't have liked that either. On 5/5/18, Michael Shulman wrote: > 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. >> >> >> >> >> >