On Sun, Aug 24, 2014 at 4:36 PM, Martin Escardo <
m.es...@cs.bham.ac.uk> wrote:
> As the bet is formulated, it would be much harder for you to win: you
> would have to cook up a model that (1) satisfies univalence (and
> perhaps interprets HIT's to be completely honest), (2) doesn't
> validate any of the above instances of excluded middle you describe,
> and, moreover, (3) has such an automorphism.
I don't think Andrej would need *one* model with all of these
properties. Wouldn't it be enough for him to describe a *class* of
models that each contain a nontrivial automorphism of U and such that
any nontrivial instance of LEM is violated in at least one of them?
> Here is a careful formulation of this question: Is there a closed type
> B (in any universe) such that (a) MLTT doesn't inhabit B, (b) MLTT+EM
> inhabits B, and (c) MLTT+univalence inhabits B.
I believe the answer to this should be yes. Here's an example:
Let U be some fixed universe, and say that a family P : A -> U is a
"fiberwise U-proposition" if Forall(x:A) isProp(P(x)). Consider the
claim
(*) There exists a type Omega and a fiberwise U-proposition T : Omega
-> U such that (1) every fiberwise U-proposition P : A -> U is
equivalent to the composite of T with some map chi_P : A -> Omega, and
(2) if the composites of T with two maps f,g : A -> Omega are
fiberwise equivalent, then f and g are homotopic.
In other words, there is a subobject classifier for U-propositions. I
propose that (*), when expressed as a closed type (which of course
belongs to the next higher universe than U), probably satisfies your
three conditions. Let's consider them in reverse order:
(c) This is the easiest: let Omega = Sum(P:U) isProp(P). Condition
(1) is true essentially by definition, and (2) follows from
propositional univalence.
(b) Let Omega = 2, with T(0)=0 and T(1)=1 (under an obvious abuse of
notation). Under LEM, any proposition is equivalent to either 0 or 1,
so a fiberwise U-proposition P : A -> U induces a map chi_P : A ->
Omega where chi_P(x) = 0 if P(x) is equivalent to 0 and chi_P(x) = 1
if P(x) is equivalent to 1, and condition (1) holds. For (2), if f(x)
is equivalent to g(x), then they must either both be equivalent to 1
or both equivalent to 0, and in either case f(x) = g(x).
(Categorically speaking, 2 is a subobject classifier in any Boolean
category.)
(a) I don't have a watertight argument for this one, but I feel that
it should clearly be true. There are certainly locally cartesian
closed categories that do not have subobject classifiers (e.g. any
quasitopos that is not a topos), but I can't right now think of any
that do have (necessarily non-univalent) universes. Maybe you could
look at something like the category of sets in a predicative set
theory with universes, but in that case I'm not sure how to prove
definitely that it doesn't have subobject classifiers (though clearly
it shouldn't).
Mike