Automorphisms of U

[Martin Escardo]

In connection with the Kraus-Sattler paper I mentioned in the other
thread, I highlight the following question, which they leave open:

What do the automorphisms of U look like?

(1) In the (univalent) models.
(2) Internally in HoTT.

I am particularly interested in (2), but any answers regarding (1) are
also welcome and should be illuminating.

(Nicolai and Christian mention (in page 11) parametricity in this
respect.)

There are plenty of interesting functions F : U → U. E.g. "type
constructors", internalized (object parts of) functors,
such as F X = A × X for any given A : U, etc.

But is there any interesting *equivalence* F : U → U, other than the
identity?

A "tiny" fraction of U is

Ω := Σ(P : U). isProp P,

where isProp P says that P is an (h)proposition (any two of its points
are equal).

Higgs' Involution Theorem for toposes says that any monomorphism Ω → Ω
is an involution (and hence an isomorphism).

In particular, any isomorphism Ω → Ω is its own inverse.

This works for type theory too, assuming univalence for propositions
(any two equivalent propositions are equal) with the above definition
of Ω, and I have checked this in Agda:
http://www.cs.bham.ac.uk/~mhe/agda/HiggsInvolutionTheorem.html

This should perhaps say something about automorphisms U → U.

I have the feeling that, once univalence is assumed, even assuming
excluded middle for propositions and more generally choice for sets,
there shouldn't be any automorphism U → U other than the identity.

Can anything to that extent be said inside type theory? Or do we need
to look at models to learn anything about that?

M.

[Peter LeFanu Lumsdaine]

On Sat, Aug 16, 2014 at 12:21 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

In connection with the Kraus-Sattler paper I mentioned in the other
thread, I highlight the following question, which they leave open:

What do the automorphisms of U look like?

I like the question!  The suggestion:

 

I have the feeling that, once univalence is assumed, even assuming
excluded middle for propositions and more generally choice for sets,
there shouldn't be any automorphism U → U other than the identity.

is certainly too strong — once we have EM for propositions, we can define a non-trivial automorphism by e.g. sending X:U to “if X is a proposition then not-X, else X”.  

More generally, we know in the simplicial model that each connected component of the universe is of the form BAut(X), i.e. the classifying space of the automorphism group of a space.  When Aut(X) has outer automorphisms (e.g. if X = 6, the famous outer automorphism of S_6), these will become non-trivial automorphisms of BAut(X), and hence extend (by acting as the identity on other components) to non-trivial automorphisms of U.

Indeed, the S_6 example (and similar ones) ought to be definable/provable, assuming EM for the proposition “X is an hset with (merely) exactly 6 elements”.  It’s not obvious (to me) how to define the non-trivial action on the intended connected component, but it surely should be possible…?

More interestingly, can an automorphism interchange connected components, beyond the trivial case of 0 and 1?  I.e. can one have types with BAut(X) = BAut(Y), without having X = Y, other than in the case of 0 and 1?  I seem to recall versions of this being discussed here before, but I don’t remember the answer.

–p.

[Michael Shulman]

On Fri, Aug 15, 2014 at 5:52 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> More interestingly, can an automorphism interchange connected components,
> beyond the trivial case of 0 and 1? I.e. can one have types with BAut(X) =
> BAut(Y), without having X = Y, other than in the case of 0 and 1? I seem to
> recall versions of this being discussed here before, but I don’t remember
> the answer.

If X and Y are both rigid, then this should be true, right?

[andré hirschowitz]

Hello,

What do the automorphisms of U look like?

  (1) In the (univalent) models.

Anthony Bordg is currently checking the final details of the construction of a univalent model where the universe comes equipped with a nontrivial involution. His construction should generalize easily to the case of any group. However, in this construction, the group action is trivial on connected components.

ah

Note: the fact that the involution is not trivial relies completely on the fact that the meta-theory (ZFC say) is not univalent.

[Peter LeFanu Lumsdaine]

Ah, yes!  So this now gives (assuming univalence and HITs) uncountably many non-trivial automorphisms of U, since we have at least countably many rigid types (K(S_n,1), for n ≠ 6), which (assuming EM_prop) can be permuted at will.  

(Previous threads on rigid types: http://goo.gl/JxgyIt and http://goo.gl/HSJTkh)

So we now have two classes of examples, both definable and provably non-trivial assuming EM_prop:

(a) permuting the trivial connected components (i.e. the components of rigid types)

(b) acting non-trivially on non-trivial connected components.

Do we have any examples that either:

(c) interchange non-trivial connected components?  (i.e. can we find non-rigid types with the same BAut(X)?)

(d) are at least definable, and hopefully provably non-trivial, without assuming any EM?

–p.

[Zhen Lin]

On 16 August 2014 11:15, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

(c) interchange non-trivial connected components?  (i.e. can we find non-rigid types with the same BAut(X)?)

Surely, yes? Classically, at least, we could take the disjoint union of two copies of the same rigid type, and the resulting type would have the two-element group as its automorphism group.

[Peter LeFanu Lumsdaine]

Hmm — we have to be a little more careful; e.g. if the rigid type is 0, this doesn’t work; or if it’s 1 + R where R is some rigid K(G,1), G≠0.  But I think with a *connected* rigid type, this works.

Generally, I guess, if R is an n-connected rigid type and X is an n-type, then Aut(R) = Aux(R x X)?

–p.

[Michael Shulman]

On Sat, Aug 16, 2014 at 3:15 AM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> (d) are at least definable, and hopefully provably non-trivial, without
> assuming any EM?

To this one I could believe the answer might be "no". It reminds me
of parametricity and the fact that the universe is "indiscrete" (in
the internal sence defined by "convergence of sequences" using maps
out of N_oo), although I don't yet see that it follows from either
one.

[andré hirschowitz]

hi Martin,

After all, I am not sure I have correctly understood your question:

What do the automorphisms of U look like?

  (1) In the (univalent) models.

 

My understanding has been: in a (univalent) model we have an underlying category M equipped with an object U (the interpretation of the univalent universe) and the question is what can be the automorphism group of U in M.
 I even understood that your hope was that this group was always trivial. Was I right? Or what else?

BTW, thanks to private comments by Mike Shulman, I now suspects that Anthony's construction will extend to the case of arbitrary commutative groups only.

ah

[Martin Escardo]

On 16/08/14 23:52, andré hirschowitz wrote:
> hi Martin,
>
>
> After all, I am not sure I have correctly understood your question:
>
>
> What do the automorphisms of U look like?
>
> (1) In the (univalent) models.
>
>
>
> My understanding has been: in a (univalent) model we have an underlying
> category M equipped with an object U (the interpretation of the
> univalent universe) and the question is what can be the automorphism
> group of U in M.
> I even understood that your hope was that this group was always
> trivial. Was I right? Or what else?

I don't think you need to think of U as a group object in some category.

Any type in Martin-Loef type theory is a groupoid, and hence U in
particular is a groupoid.

In any case for any two types X and Y you have the notion of
equivalence, a function X -> Y whose fibers are contractible (among
other possible definitions, any of which can be taken as primitive - see
the HoTT book).

By an automorphism of U we simply mean an equivalence U -> U.

There are two questions: (1) whether in some models there are
interesting examples, (2) whether in (the syntax of) HoTT one can define
any equivalence U -> U other than the identity.

To summarize what other people said in this thread: regarding (1), there
are indeed examples other than the identity in some models; regarding
(2), nobody knows, but we suspect that without excluded middle there
shouldn't be any *definable* equivalence U -> U.

I hope this clarifies what has been asked.

M.

> BTW, thanks to private comments by Mike Shulman, I now suspects that
> Anthony's construction will extend to the case of arbitrary commutative
> groups only.
>
> ah

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Michael Shulman]

I think Andre's question is rather about whether the notion of
equivalence in question is internal or external. For any type A, we
have the type Eq(A,A) of self-equivalences of A, and I assumed that
the questions were (1) in models, are there terms belonging to Eq(U,U)
that are not (propositionally) equal to the identity, and (2) can we
construct such a term without additional hypotheses?

But I think Andre is asking about whether question (1) was rather
about the of automorphisms of U as an object of the underlying
category in some model. For instance, in the simplicial set model,
there might be an automorphism of the base of the universal Kan
fibration, as an object of sSet, which is not equal (in sSet) to the
identity, but which is *homotopic* to the identity, and hence equal to
it as an element of Eq(U,U).

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Martin Escardo]

Just one quick comment, Mike:

On 16/08/14 18:44, Michael Shulman wrote:
> On Sat, Aug 16, 2014 at 3:15 AM, Peter LeFanu Lumsdaine
> <p.l.lu...@gmail.com> wrote:
>> (d) are at least definable, and hopefully provably non-trivial, without
>> assuming any EM?
>

> To this one I could believe the answer might be "no". '

I concur.

> It reminds me of parametricity

(Which is already mentioned in the Kraus-Sattler paper.)

> and the fact that the universe is "indiscrete" (in the internal
> sence defined by "convergence of sequences" using maps out of N_oo),

If X is an indiscrete space, then any function X->X is continuous, and
in particular any automorphism of the underlying set of X is an
automorphism of the space X. Hence in general indiscrete spaces have
plenty of automorphisms.

Hence I think it is unlikely that the indiscreteness of U may help
here.

> although I don't yet see that it follows from either
> one.

I am also skeptical about parametricity, but I am not able to say why,
other than I tried it but I don't see any way how it can be applied:
there are plenty of (non-trivial and interesting) functions U -> U,
but I don't see (at least the moment) what is special, in relation to
parametricity, about those which are equivalences.

I would rather fish for a taboo, internally derived: the existence of
a non-trivial automorphism should imply an instance of excluded middle
(conversely, as Peter said, with EM we can define an automorphism) .
But again I didn't succeed in that direction (yet).



Martin

[Nicolai Kraus]

On 21/08/14 20:10, Martin Escardo wrote:
> Just one quick comment, Mike:
>
> On 16/08/14 18:44, Michael Shulman wrote:
>> On Sat, Aug 16, 2014 at 3:15 AM, Peter LeFanu Lumsdaine
>> <p.l.lu...@gmail.com> wrote:
>>> (d) are at least definable, and hopefully provably non-trivial, without
>>> assuming any EM?
>>
>> To this one I could believe the answer might be "no". '
>
> I concur.
>
>> It reminds me of parametricity
>
> (Which is already mentioned in the Kraus-Sattler paper.)

Another quick comment: Asking for a nontrivial automorphism on the
universe U corresponds to asking for a nontrivial element of the loop
space Omega(V,U) [where V is just any larger universe].
If you ask for nontrivial elements of Omega^2(V,U) instead, it reminds
even more of parametricity, because Omega^2(V,U) is equivalent to Pi
(X:U). X=X, and to find an inhabitant of that is at least as hard as for
Pi (X:U). X -> X.

> I would rather fish for a taboo, internally derived: the existence of
> a non-trivial automorphism should imply an instance of excluded middle
> (conversely, as Peter said, with EM we can define an automorphism) .
> But again I didn't succeed in that direction (yet).

Martin, if you can get a taboo from that, I would be very interested!
Nicolai

[Martin Escardo]

On 21/08/14 20:47, Nicolai Kraus wrote:
> Another quick comment: Asking for a nontrivial automorphism on the
> universe U corresponds to asking for a nontrivial element of the loop
> space Omega(V,U) [where V is just any larger universe].
> If you ask for nontrivial elements of Omega^2(V,U) instead, it reminds
> even more of parametricity, because Omega^2(V,U) is equivalent to Pi
> (X:U). X=X, and to find an inhabitant of that is at least as hard as for
> Pi (X:U). X -> X.

Nice. So I am less skeptical about the applicability of parametricity to
this question.

Martin

[Andrej Bauer]

On Thu, Aug 21, 2014 at 9:10 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> I would rather fish for a taboo, internally derived: the existence of
> a non-trivial automorphism should imply an instance of excluded middle

I bet one evening's worth of beers that you can derive no instance of
excluded middle from having a non-trivial automorphism of the
universe.

By "non-trivial" instance I mean one that can't already be derived.

"Non-trivial" automorphism can be a number of things. Let's take a
fairly strong notion: we assume there is an automorphism f of U and a
type A : U such that A is not equivalent to f(A).

With kind regards,

Andrej

[Martin Escardo]

When thinking about your bet, I encountered a difficulty that I had
not anticipated.

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.

The problem is that there are (h)propositions A such that (i) A
implies the negation of excluded middle, and yet (ii) A implies
consequences of excluded middle that are not provable.

One example is A=(all functions (N->2)->N are uniformly continuous).

(i) From A you conclude the negation of excluded middle. (For if EM
holds then you can define a non-continuous function (N->2)->N.)

(ii) From A you conclude that for all f:(N->2)->N either f(a)=0 for
some a:N->2 or not (by induction on the minimal modulus of uniform
continuity of f), which is an instance of excluded middle that is
not provable in MLTT.

Your model would have to falsify all such propositions A (not just
uniform continuity).

But the situation may be even worse in principle: certainly univalence
doesn't imply the negation of excluded middle, but (ii) does it imply
consequences of excluded middle that are not provable without it?

This, if it were the case, wouldn't be necessarily "bad": uniform
continuity does imply such an instance, and yet it has a computational
model (at least without univalence, but hopefully with it too).

Hence, not only would it be difficult for you to win, but also it
would be difficult for you to assess that I've won when I propose a
solution, for the instance of excluded middle I produce from the
assumption of an automorphism of U may well be, in principle, an
instance of excluded middle derivable from univalence alone. How can
you (or I) be sure?

Question: does univalence imply any instance of excluded middle that
is not already provable in MLTT?

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.

As I said above, I would fish for a taboo. Should I? Should I accept
Andrej's bet?

Best,
Martin

[Peter LeFanu Lumsdaine]

As I said above, I would fish for a taboo. Should I? Should I accept
Andrej's bet?

My intuition agrees with Andrej’s — it seems to me unlikely one can derive a taboo, though also as you say, it would be hard to prove one can’t!

Here’s even a slightly stronger hypothesis to try working from:

- There is an auto-equivalence of U that interchanges 0 and 1.

It seems much more plausible to me that one could get a taboo from this — but I still haven’t been able to.  Can you?

–p.

[Michael Shulman]

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

[Michael Shulman]

On Sun, Aug 24, 2014 at 5:52 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> - There is an auto-equivalence of U that interchanges 0 and 1.
>
> It seems much more plausible to me that one could get a taboo from this —
> but I still haven’t been able to. Can you?

This is not the same as a taboo, but I claim that any *definable*
automorphism of U (in MLTT+univalence) must fix 0.

If F : U -> U is definable, then it exists in every model, and
moreover is preserved by every strict morphism of models. In
particular, it exists in the Sierpinski model built over the syntactic
model, whose objects consist of a closed type and a type family over
it:

|- A0 type
(a0 : A0) |- A1 type

In this model, the universe induced by a universe U in the syntactic model is

|- U type
(A0 : U) |- (A0 -> U) type

Thus, if F : U -> U is a definable equivalence, then it induces an
automorphism of this object in the Sierpinski model, which consists of
(1) an equivalence F0 : U -> U, and (2) a family of equivalences
F1(A0) : (A0 -> U) -> (F0(A0) -> U) for all A0:U. Moreover, since
there is a strict functor from the Sierpinski model to the syntactic
model that remembers only the type A0, the equivalence F0 must in fact
be F.

Now let A0 = 0; then F1(0) is an equivalence from (0 -> U) to (F(0) ->
U). However, the type (X -> U) is contractible if and only if X=0:
"if" is obvious; while conversely if (X -> U) is contractible and we
have x:X, then
0 = (lam _.0)(x) = (lam _.1)(x) = 1
hence X is empty. Thus, F(0)=0.

I feel like it should be possible to push this sort of argument
further, but so far I haven't been able to.

Mike

[Andrej Bauer]

On Mon, Aug 25, 2014 at 1:36 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> As the bet is formulated, it would be much harder for you to win:

That's all right, we'll both be inclined to concede because the reward
will be beer. You should accept the challenge, but not in the form
that Peter suggested (0 and 1 switched) because that's too strong.

With kind regards,

Andrej

[Martin Escardo]

Lemma. Excluded middle holds iff every proposition is (logically
equivalent to) the negation of some type.

I leave this as an easy exercise (use excluded middle in the form
not-not P -> P for all propositions P, and the fact that not-not-not X
-> not X for any type X).

Now suppose that you have a left-cancellable map f:U->U with f(1)=0
and suppose that univalence holds for propositions.

Let P be any proposition. Then

P <-> P = 1 by propositional univalence
<-> f(P)=f(1) because f is left-cancellable
<-> f(P)=0 because f(1)=0
<-> not f(P) by propositional univalence.

Hence every proposition P is the negation of the type f(P), and, by
the lemma, excluded middle holds.

Putting this together with an argument by Peter in an earlier message:

Theorem. There is an automorphism of U that exchanges 0 and 1 iff
excluded middle holds.

So we get the strongest possible taboo in Peter's special case of the
question.

Martin

[Peter LeFanu Lumsdaine]

On Mon, Aug 25, 2014 at 11:27 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> Theorem. There is an automorphism of U that exchanges 0 and 1 iff
excluded middle holds.
> 
> So we get the strongest possible taboo in Peter's special case of the
question.

Very nice!  And it generalises at least a little bit, to cover some of the other automorphisms we discussed — those exchanging 0 with some other inhabited rigid type, not necessarily 1.

Lemma. Let P be a proposition, and A any merely-inhabited (i.e. (–1)-connected) type.  Then P <–> (P*A = A).  (Note this is just bi-implication, not necessarily equivalence; A need not be rigid.)

Proof:

(–>)  P   –>   P = 1   –>   P * A = A;

(<–)  P * A = A   –>   |P * A| = 1   –>   |P|*|A| = 1   –>   P = 1.

Lemma: If F is a merely left-cancellable function on U with F(A) = 0 for some merely inhabited type A, then EM holds.

Proof: for any proposition P, we have bi-implications

P <–> P * A = A

   <–> F(P*A) = F(A)

   <–> F(P*A) = 0

   <–> not F(P*A)

As in Martin’s previous email, EM follows.

Corollary: EM holds iff there is an automorphism of U exchanging 0 with some merely inhabited type.

Now, how can we weaken this assumption further?

–p.

[Andrej Bauer]

On Mon, Aug 25, 2014 at 11:51 AM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> Corollary: EM holds iff there is an automorphism of U exchanging 0 with some
> merely inhabited type.
>
> Now, how can we weaken this assumption further?

Well, since only left-cancelable maps are used throughout:

Theorem: EM holds iff there is an "embedding" of the universe into
itself which maps 0 to a merely inhabited type.

I suspect "embedding" isn't quite the right word for a left-cancelable
map, is it?

Has anyone built simplicial sets over a Fraenkel-Mostowski permutation
model of ZF? It's got excluded middle but not choice, and it should
give us an automorphism of the universe, so I can have my beer.

With kind regards,

Andrej

[Martin Escardo]

Interesting, even if it is in a direction different from taboos. M.

[Thomas Streicher]

As long as one doesn't insist on univalence one can easily construct
automorphisms of universes in realizability models. Consider assemblies
obver the first Kleenea algebra (natural numbers) and take U = PER(N).
Then any recursive automorphism of N induces an isomorphism of U which
is nonidentical provided the recursive automorphism of N is nonidentical.

Thomas

[Michael Shulman]

Andrej:

> Has anyone built simplicial sets over a Fraenkel-Mostowski permutation
> model of ZF? It's got excluded middle but not choice, and it should
> give us an automorphism of the universe

and Thomas:

> Consider assemblies
> obver the first Kleenea algebra (natural numbers) and take U = PER(N).
> Then any recursive automorphism of N induces an isomorphism of U which
> is nonidentical provided the recursive automorphism of N is nonidentical.

I have the same question for you both of you that I had for André H.:
how do you know that these automorphisms are *internally* nontrivial?

[Martin Escardo]

On 25/08/14 10:51, Peter LeFanu Lumsdaine wrote:
> Corollary: EM holds iff there is an automorphism of U exchanging 0 with
> some merely inhabited type.

Nice.

(Just to make explicit something that was alluded to before: if f:U->U
is an automorphism and X is rigid, then (f(X)=f(X)) = (X = X) = 1, and
so f(X) is rigid too. This shows, in particular, that f(0) is rigid
and any type with f(X)=0 is rigid.)

> Now, how can we weaken this assumption further?

I was trying to replace "merely inhabited" by "non-empty", but I
haven't succeeded (yet?).

In case of success, one gets as a consequence that f(0)/=0 if and only
if EM holds.

Martin

[Martin Escardo]

Interesting, Mike. Thanks, Martin

[Martin Escardo]

Ok, but we may end up having that beer before the bet is settled.

Best,
Martin

[Michael Shulman]

This is a cute argument. Basically, if F(A)=0 for some merely
inhabited A, then F is "enough like negation" that it can be used to
show that negation is surjective, and hence an involution.

[Martin Escardo]

On 25/08/14 10:51, Peter LeFanu Lumsdaine wrote:

> Corollary: EM holds iff there is an automorphism of U exchanging 0 with
> some merely inhabited type.

You can equivalently say EM holds iff there is an automomorphism
f:U->U with ||f(0)||.

Negating both sides of the logical equivalence of the corollary, and
remembering that

not || Y || <-> not Y <-> Y = 0,

under propositional univalence, we get

Corollary. TFAE in MLTT + ||-|| + propositional-univalence:

(1) The negation of EM.
(2) f(0)=0 for every equivalence f:U->U.

(It is mildly annoying that we have to assume the type constructor
||-||, because it only occurs in the proof of the theorem and not its
formulation. This is why I was trying to generalize Peter's corollary
from "merely inhabited" to "non-empty".)

Martin

[Andrew Polonsky]

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.

How about

{UA} + {~ UA}  ?

Andrew

[Michael Shulman]

Much easier than my example! But there is still the problem of
verifying the "obvious" fact (a)...

[Andrew Polonsky]

On Mon, Aug 25, 2014 at 7:57 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> Much easier than my example! But there is still the problem of
> verifying the "obvious" fact (a)...

By canonicity, if (a) fails, either MLTT |- UA or MLTT |- ~UA. The
set-theoretic model, where identity is interpreted by exact equality,
refutes the former. The simplicial model refutes the latter.

Andrew

[Michael Shulman]

Ah, of course.

[Martin Escardo]

Nice!

So whenever you postulate an undecided axiom, you also get an instance
of excluded middle which was not provable. (Obvious in retrospect!)

Martin

[Thomas Streicher]

> I have the same question for you both of you that I had for André H.:
> how do you know that these automorphisms are *internally* nontrivial?

In the case of realizability the automorphism i : U -> U validates
that A and i(A) are isomorphic for A:U but they are not equal (it's a
model of extensional type theory).

Thomas

[Michael Shulman]

Okay, so if we extended that model to a univalent one somehow, then we
would expect that they would become equal, so that the automorphism
would be trivial.

[Martin Escardo]

Let's modify Andrej's bet slightly, so that we don't need to wait a
long time until somebody wins.

If from an arbitrary equivalence f:U->U such that f(X) /= X for a
particular X:U you get a non-provable consequence of EM, then you get
X-many beers.

So far, from the argument below, Peter L. and I get 0 beers, because
from f(0) /= 0 we get the taboo not-not EM. Although perhaps sober,
this is, I think, a nice achievement.

(Of course not-not EM follows from EM and is (should) not be provable
in MLTT from ||-|| and propositional univalence, and so realy is (or
better should be) a taboo.)

(I would have liked to derive EM from f(0)/=0, but so far I can only
derive not-not EM, with the arguments already shown in this thread.)

To get 1 beer, you need to start with an arbitrary equivalence f:U->U
and the assumption f(1) /= 1, and derive a consequence of EM that is
not derivable without this assumption.

Can anyone get 1 beer?

Martin