From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.46.21.65 with SMTP id 1mr2530622ljv.4.1484423570090;
        Sat, 14 Jan 2017 11:52:50 -0800 (PST)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.25.157.8 with SMTP id g8ls399595lfe.39.gmail; Sat, 14 Jan 2017
 11:52:48 -0800 (PST)
X-Received: by 10.25.40.17 with SMTP id o17mr1376297lfo.25.1484423568768;
        Sat, 14 Jan 2017 11:52:48 -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 d130si376504wmf.0.2017.01.14.11.52.48
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Sat, 14 Jan 2017 11:52:48 -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.54] (helo=mailer3)
	by sun60.bham.ac.uk with esmtp (Exim 4.84)
	(envelope-from <escardo...@googlemail.com>)
	id 1cSUNc-0000S9-OL
	for HomotopyT...@googlegroups.com; Sat, 14 Jan 2017 19:52:48 +0000
Received: from [31.185.232.183] (helo=[192.168.1.128])
	by bham.ac.uk (envelope-from
	<escardo...@googlemail.com>)
	with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128)
	(Exim 4.84)
	id 1cSUNc-0002Bi-EO
	for HomotopyT...@googlegroups.com 
	using interface auth-smtp.bham.ac.uk; Sat, 14 Jan 2017 19:52:48 +0000
Subject: Re: [HoTT] new preprint available
To: "HomotopyT...@googlegroups.com"
 <HomotopyT...@googlegroups.com>
References: <C79A5055-7559-4E00-8217-E87C703E28FF@chalmers.se>
From: Martin Escardo <escardo...@googlemail.com>
Message-ID: <60244690-d027-1a0b-2796-3e898028b4b2@googlemail.com>
Date: Sat, 14 Jan 2017 19:52:48 +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: <C79A5055-7559-4E00-8217-E87C703E28FF@chalmers.se>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
X-BHAM-SendViaRouter: yes
X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom)

On 11/01/17 08:58, Thierry Coquand wrote:
>
>  A new preprint is available on arXiv
>
> http://arxiv.org/abs/1701.02571
>
> where we present a stack semantics of type theory, and use it to
> show that countable choice is not provable in dependent type theory
> with one univalent universe and propositional truncation.

Nice. And useful to know.

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.)

We know that countable choice is not provable from excluded middle.

But the above instance is. (And much less than excluded middle is enough.)

Best,
Martin