Re: [HoTT] new preprint available

[Martin Escardo <escardo...@googlemail.com>]

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