57 views

Skip to first unread message

Aug 15, 2014, 7:21:36 PM8/15/14

to HomotopyT...@googlegroups.com

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.

Aug 15, 2014, 8:52:41 PM8/15/14

to Martin Escardo, HomotopyT...@googlegroups.com

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.

Aug 16, 2014, 12:32:51 AM8/16/14

to Peter LeFanu Lumsdaine, Martin Escardo, HomotopyT...@googlegroups.com

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

Aug 16, 2014, 6:03:05 AM8/16/14

to Martin Escardo, HomotopyT...@googlegroups.com

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.

Aug 16, 2014, 6:15:54 AM8/16/14

to Michael Shulman, Martin Escardo, HomotopyT...@googlegroups.com

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.

Aug 16, 2014, 6:49:36 AM8/16/14

to Peter LeFanu Lumsdaine, Michael Shulman, Martin Escardo, HomotopyT...@googlegroups.com

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.

Aug 16, 2014, 7:24:56 AM8/16/14

to Zhen Lin, Michael Shulman, Martin Escardo, HomotopyT...@googlegroups.com

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.

Aug 16, 2014, 1:44:33 PM8/16/14

to Peter LeFanu Lumsdaine, Martin Escardo, HomotopyT...@googlegroups.com

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
<p.l.lu...@gmail.com> wrote:

> (d) are at least definable, and hopefully provably non-trivial, without

> assuming any EM?

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.

Aug 16, 2014, 6:52:47 PM8/16/14

to Martin Escardo, HomotopyT...@googlegroups.com

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

Aug 17, 2014, 2:48:32 PM8/17/14

to andré hirschowitz, HomotopyT...@googlegroups.com

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?

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

--
> Anthony's construction will extend to the case of arbitrary commutative

> groups only.

>

> ah

Martin Escardo

http://www.cs.bham.ac.uk/~mhe

Aug 17, 2014, 5:30:19 PM8/17/14

to Martin Escardo, andré hirschowitz, HomotopyT...@googlegroups.com

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.

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.

Aug 21, 2014, 3:10:58 PM8/21/14

to Michael Shulman, Peter LeFanu Lumsdaine, HomotopyT...@googlegroups.com

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

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?

>

I concur.

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

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.

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

Aug 21, 2014, 3:47:58 PM8/21/14

to HomotopyT...@googlegroups.com

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

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

Nicolai

Aug 21, 2014, 4:55:48 PM8/21/14

to Nicolai Kraus, HomotopyT...@googlegroups.com

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.

this question.

Martin

Aug 24, 2014, 3:42:58 PM8/24/14

to HomotopyT...@googlegroups.com

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
> I would rather fish for a taboo, internally derived: the existence of

> a non-trivial automorphism should imply an instance of excluded middle

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

Aug 24, 2014, 7:36:59 PM8/24/14

to Andrej Bauer, HomotopyT...@googlegroups.com

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

Aug 24, 2014, 8:52:43 PM8/24/14

to Martin Escardo, Andrej Bauer, HomotopyT...@googlegroups.com

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.

Aug 25, 2014, 12:52:13 AM8/25/14

to Martin Escardo, Andrej Bauer, HomotopyT...@googlegroups.com

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

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.

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

Aug 25, 2014, 1:07:35 AM8/25/14

to Peter LeFanu Lumsdaine, Martin Escardo, Andrej Bauer, HomotopyT...@googlegroups.com

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*
<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?

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

Aug 25, 2014, 2:52:16 AM8/25/14

to HomotopyT...@googlegroups.com

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
> As the bet is formulated, it would be much harder for you to win:

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

Aug 25, 2014, 4:27:14 AM8/25/14

to Peter LeFanu Lumsdaine, Andrej Bauer, HomotopyT...@googlegroups.com

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

Aug 25, 2014, 5:51:51 AM8/25/14

to Martin Escardo, Andrej Bauer, HomotopyT...@googlegroups.com

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

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.

Aug 25, 2014, 6:23:31 AM8/25/14

to HomotopyT...@googlegroups.com

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:
<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?

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

Aug 25, 2014, 9:54:16 AM8/25/14

to Michael Shulman, Peter LeFanu Lumsdaine, Andrej Bauer, HomotopyT...@googlegroups.com

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

Aug 25, 2014, 10:33:42 AM8/25/14

to Martin Escardo, Michael Shulman, Peter LeFanu Lumsdaine, Andrej Bauer, HomotopyT...@googlegroups.com

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

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

Aug 25, 2014, 11:22:24 AM8/25/14

to Thomas Streicher, Andrej Bauer, HomotopyT...@googlegroups.com

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?

> 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

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

how do you know that these automorphisms are *internally* nontrivial?

Aug 25, 2014, 11:25:14 AM8/25/14

to Peter LeFanu Lumsdaine, Andrej Bauer, HomotopyT...@googlegroups.com

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.

(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?

haven't succeeded (yet?).

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

if EM holds.

Martin

Aug 25, 2014, 11:26:15 AM8/25/14

to Michael Shulman, Andrej Bauer, HomotopyT...@googlegroups.com

Interesting, Mike. Thanks, Martin

Aug 25, 2014, 11:27:51 AM8/25/14

to Andrej Bauer, HomotopyT...@googlegroups.com

Best,

Martin

Aug 25, 2014, 11:29:02 AM8/25/14

to Martin Escardo, Peter LeFanu Lumsdaine, Andrej Bauer, HomotopyT...@googlegroups.com

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.

inhabited A, then F is "enough like negation" that it can be used to

show that negation is surjective, and hence an involution.

Aug 25, 2014, 12:17:24 PM8/25/14

to Peter LeFanu Lumsdaine, Andrej Bauer, HomotopyT...@googlegroups.com

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
> some merely inhabited type.

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

Aug 25, 2014, 12:53:30 PM8/25/14

to HomotopyT...@googlegroups.com, andrej...@andrej.com

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

Aug 25, 2014, 12:57:41 PM8/25/14

to Andrew Polonsky, homotopyt...@googlegroups.com

Much easier than my example! But there is still the problem of

verifying the "obvious" fact (a)...

verifying the "obvious" fact (a)...

Aug 25, 2014, 1:00:32 PM8/25/14

to Michael Shulman, homotopyt...@googlegroups.com

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
> Much easier than my example! But there is still the problem of

> verifying the "obvious" fact (a)...

set-theoretic model, where identity is interpreted by exact equality,

refutes the former. The simplicial model refutes the latter.

Andrew

Aug 25, 2014, 1:04:18 PM8/25/14

to Andrew Polonsky, homotopyt...@googlegroups.com

Ah, of course.

Aug 25, 2014, 1:08:08 PM8/25/14

to Andrew Polonsky, HomotopyT...@googlegroups.com, andrej...@andrej.com

So whenever you postulate an undecided axiom, you also get an instance

of excluded middle which was not provable. (Obvious in retrospect!)

Martin

Aug 25, 2014, 3:28:44 PM8/25/14