From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a0c:f989:: with SMTP id t9-v6mr19138089qvn.27.1525555672464; Sat, 05 May 2018 14:27:52 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:dd85:: with SMTP id v5-v6ls6733687qvk.3.gmail; Sat, 05 May 2018 14:27:51 -0700 (PDT) X-Received: by 2002:a0c:9345:: with SMTP id e5-v6mr19469096qve.15.1525555671686; Sat, 05 May 2018 14:27:51 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525555671; cv=none; d=google.com; s=arc-20160816; b=yvpPgPNMmkVncbKbsDKT4A+qKFvmPlbtSgDnsWwHI/tYebd39lBmf/L5WHhf7av1Bf YdDNok0uGiLcgLgR0/hm0YInxB7Xb7hNEc0a6an/2C7gGCBOAOs1vEqeS7vZoavf4YWg tvCVzqlPkTAOHW2/vRuOgN6PUBAYMjGn+pD6Q9J2e9InjXeyA/QLjJvO4jz3b+GXaEfr 9kaDRGgDNO2ZpD0IDsXxfyn4rItT6mvMKTwPL+a307ht1JUT1NO/zVt59nYUMREn8gyK tc+NqNVkxGlBMf8WXyR4ZRiVxJITRS8AVzHHxjTLT72PmYZe7xGmfL5fBYjJC3izvtOj 6sSQ== 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=Ra6L4mC0mvSPGqBuKpu4eWqaibNDEf+cidTEvTDktug=; b=hUsV2ZSgVYolMq9QaNJJl4aCPd1TMxdbg97nAPFLjX098q64MyTalvse36NP5eA/br q0dODE0ZeBQWECZYYncGtPM9Q3umqp3A5brXin+Umf79g299mQX0oTuMfWxvoDo4YWA2 nVfHzfJe0aNhpNQKTY8HlgQZPSV0SZHESWnp4mJgocTG030/oTzrh5ugIcXTAWNCytCy OoR2Zmit5j5QdZDlLfV83YvW3pCfsH4Edl+BO0JI7sQJerSYWdU1NZR4XMlmQdWYz6pS 93HcnepPxgznPf7XGQNws+4YXc1uZOuxwF0lk73dgeztUGWB9hS453WZCZa6l5BNmDXK H86g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=nkBCVETz; spf=neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x233.google.com (mail-yw0-x233.google.com. [2607:f8b0:4002:c05::233]) by gmr-mx.google.com with ESMTPS id d67si996140qkh.5.2018.05.05.14.27.51 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 05 May 2018 14:27:51 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=nkBCVETz; spf=neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x233.google.com with SMTP id l15-v6so7652650ywk.3 for ; Sat, 05 May 2018 14:27:51 -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=Ra6L4mC0mvSPGqBuKpu4eWqaibNDEf+cidTEvTDktug=; b=nkBCVETzxwE+43zYKelkXnNPtBUoBedhS6Bxnd9Hht0ruaCDR3i3PUyc/pa53ltItV FOsAcYmAgYHH0+Sl8Tw9oSarWQUZ5thKJ2hrD8HY1dQLbxNaO/V5WFMOmZNpwN6PNtW/ Qdmx+lOpWiEs4QcMyGrHOYDsFIysTJcZN7TXEJQrRb/Vi9Bt0FGTQ/SzNmuPtVNlfsHv XX1kFkImrp0nhNBvM87fKZpW65O0R100umT0wNguCk5S72gjdap3JvBqqT88H1Lv9ZTG S9D8oHQIFXLsDgJYMssf7vJ5DMgjYCoWetiUKT4aC4fAayKqOfSSFT2zE4YIqzxIdYvg /Yag== X-Gm-Message-State: ALQs6tAGoWmxJ0nf8XGbLhAjEKEIIoYLx+MJuaAVlsxlSBrv2cwKQisP IM6J2YR/W+8l2RsELndGGhcKEzxX X-Received: by 2002:a81:55d2:: with SMTP id j201-v6mr17599078ywb.222.1525555671279; Sat, 05 May 2018 14:27:51 -0700 (PDT) Return-Path: Received: from mail-yb0-f171.google.com (mail-yb0-f171.google.com. [209.85.213.171]) by smtp.gmail.com with ESMTPSA id r12-v6sm8158503ywl.108.2018.05.05.14.27.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 05 May 2018 14:27:50 -0700 (PDT) Received: by mail-yb0-f171.google.com with SMTP id x145-v6so7971298ybg.10 for ; Sat, 05 May 2018 14:27:50 -0700 (PDT) X-Received: by 2002:a25:d894:: with SMTP id p142-v6mr3702657ybg.290.1525555669906; Sat, 05 May 2018 14:27:49 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d297:0:0:0:0:0 with HTTP; Sat, 5 May 2018 14:27:48 -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 14:27:48 -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" 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 take that back: this doesn't lead to an infinite sequence, instead it stops after one iteration, at a result that coincides with (1): > 1. Use propositions as types, as in MLTT Type-valued setoids and the > ex/lex completion. After all, "a proposition is a setoid in which any two elements are equal" is essentially the same as "a proposition is a type". This is of course a perfectly good way to get a category of setoids (although from a semantic point of view it is too limiting, restricting you to categories that arise as ex/lex completions), and I believe it's how a lot of people have interpreted Bishop's mathematics inside MLTT (for instance). But unless I'm confused, it's not what Bishop is trying to do in this manuscript; he definitely seems to want the equality relations of his setoids to be proof-irrelevant predicates.