From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.25.156.197 with SMTP id f188mr2692992lfe.14.1484562758482;
        Mon, 16 Jan 2017 02:32:38 -0800 (PST)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.46.13.18 with SMTP id 18ls957878ljn.53.gmail; Mon, 16 Jan 2017
 02:32:37 -0800 (PST)
X-Received: by 10.46.78.26 with SMTP id c26mr335518ljb.20.1484562757709;
        Mon, 16 Jan 2017 02:32:37 -0800 (PST)
Return-Path: <escardo...@googlemail.com>
Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137])
        by gmr-mx.google.com with ESMTPS id d130si692567wmf.0.2017.01.16.02.32.37
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 16 Jan 2017 02:32:37 -0800 (PST)
Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137;
Authentication-Results: gmr-mx.google.com;
       spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com;
       dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com
Received: from [147.188.128.127] (helo=bham.ac.uk)
	by sun60.bham.ac.uk with esmtp (Exim 4.84)
	(envelope-from <escardo...@googlemail.com>)
	id 1cT4ab-00013p-O1
	for HomotopyT...@googlegroups.com; Mon, 16 Jan 2017 10:32:37 +0000
Received: from mx1.cs.bham.ac.uk ([147.188.192.53])
	by bham.ac.uk (envelope-from
	<escardo...@googlemail.com>)
	with esmtp (Exim 4.84)
	id 1cT4ab-0000Ov-EC
	for HomotopyT...@googlegroups.com 
	using interface smart1.bham.ac.uk; Mon, 16 Jan 2017 10:32:37 +0000
Received: from dynamic200-118.cs.bham.ac.uk ([147.188.200.118])
	by mx1.cs.bham.ac.uk with esmtp (Exim 4.51)
	id 1cT4ab-0007mq-Eo
	for HomotopyT...@googlegroups.com; Mon, 16 Jan 2017 10:32:37 +0000
Subject: Re: [HoTT] new preprint available
To: "HomotopyT...@googlegroups.com"
 <HomotopyT...@googlegroups.com>
References: <C79A5055-7559-4E00-8217-E87C703E28FF@chalmers.se>
 <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com>
From: Martin Escardo <escardo...@googlemail.com>
Message-ID: <204f54d4-02bf-ee74-abe8-8efdb28a0d15@googlemail.com>
Date: Mon, 16 Jan 2017 10:35:33 +0000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101
 Thunderbird/45.5.1
MIME-Version: 1.0
In-Reply-To: <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com>
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 7bit
X-BHAM-SendViaRouter: yes

On 14/01/17 19:52, Martin Escardo wrote:
> I wonder whether your model, or a suitable adaptation, can prove
> something stronger, namely that a weakening of countable choice is
> already not provable. (We can discuss in another opportunity why this is
> interesting and how it arises.)
> 
> The weakening is
> 
>    ((n:N) -> || A n + B ||) -> || (n:N) -> A n + B ||
> 
> where A n is a decidable proposition and B is a set.
> 
> (Actually, the further weakening in which B is an arbitrary subset of
> the Cantor type (N->2) is also interesting. It would also be interesting
> to know whether it is provable. I suspect it isn't.)

I would like to remark that this principle is equivalent to another
choice principle.

Let *propositional choice* be the principle

Pi(P:U), isProp P -> Pi(X:P->U), (Pi(p:P), isSet(X(p)) ->
  (Pi(p:P), ||X(p)||) -> ||Pi(p:P), X(p)||.

This is equivalent to

Pi(P,Y:U), isProp P -> isSet(Y) ->
  (P  ->  ||Y||) -> ||P -> Y||.

Hence we see that it holds for decidable P, and thus holds for all P if
excluded middle holds.

The above countable choice principle is equivalence to propositional
choice with P of the form

  Sigma(n:N).a(n)=0

with a:N->2 and

  isProp(Sigma(n:N), a(n)=0).

(The statement that all such P are decidable is called LPO.)

Martin