11 views

Skip to first unread message

Oct 27, 2016, 11:15:45 AM10/27/16

to homotopytypetheory

Dear all,

we've been stuck with N. Tabareau and his student Théo Winterhalter on the above question. Is it the case that all equivalences between a universe and itself are equivalent to the identity? We can't seem to prove (or disprove) this from univalence alone, and even additional parametricity assumptions do not seem to help. Did we miss a counterexample? Did anyone investigate this or can produce a proof as an easy corollary? What is the situation in, e.g. the simplicial model?

-- Matthieu

Oct 27, 2016, 11:19:14 AM10/27/16

to Matthieu Sozeau, homotopytypetheory

There was a proof in this list that if you have excluded middle than

there is an automorphism of U that flips the types 0 and 1. (Peter

Lumsdaine.)

And conversely that if there is an automorphism that flips the types 0

and 1, then excluded middle holds. (Myself.)

Hence "potentially" there are at least two automorphisms of U.

Martin

> --

> 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

> <mailto:HomotopyTypeThe...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.

there is an automorphism of U that flips the types 0 and 1. (Peter

Lumsdaine.)

And conversely that if there is an automorphism that flips the types 0

and 1, then excluded middle holds. (Myself.)

Hence "potentially" there are at least two automorphisms of U.

Martin

> 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

> <mailto:HomotopyTypeThe...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.

Oct 27, 2016, 11:38:30 AM10/27/16

to Matthieu Sozeau, homotopytypetheory

On 27/10/16 16:19, 'Martin Escardo' via Homotopy Type Theory wrote:

> There was a proof in this list that if you have excluded middle than

> there is an automorphism of U that flips the types 0 and 1. (Peter

> Lumsdaine.)

either what Peter said or very similar to it.

To define such an automorphism f:U->U, given X:U, we have that X=0 and

X=1 are propositions. Hence we can use excluded middle to check if any

them holds, and define f(X) accordingly. Otherwise take f(X)=X.

> And conversely that if there is an automorphism that flips the types 0

> and 1, then excluded middle holds. (Myself.)

https://groups.google.com/d/msg/homotopytypetheory/8CV0S2DuOI8/Jn5EeSwxc4gJ

Martin

Oct 27, 2016, 1:08:32 PM10/27/16

to Matthieu Sozeau, Prof. Vladimir Voevodsky, homotopytypetheory

In the univalent simplicial model it is not contractible at all. For example Type_i has many connected components that are contractible and any permutation of these components is an equivalence of the ambient type.

This implies that iscontr (weq Type_i Type_i) is not provable in any context that is compatible with the univalent simplicial model.

Vladimir.

--

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.

Oct 27, 2016, 1:09:08 PM10/27/16

to Martin Escardo, Matthieu Sozeau, homotopytypetheory

On Thu, Oct 27, 2016 at 4:38 PM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote:

On 27/10/16 16:19, 'Martin Escardo' via Homotopy Type Theory wrote:

> There was a proof in this list that if you have excluded middle than

> there is an automorphism of U that flips the types 0 and 1. (Peter

> Lumsdaine.)

I can't find the link to this proof.

Martin, I guess you mean:

https://groups.google.com/d/msg/homotopytypetheory/8CV0S2DuOI8/ZvS9S-gROfIJ

In your formulation of the construction, you can swap any
two given types A and B, not only 0 and 1. This is because you really only need to decide ||X = A|| and ||X = B||.

-- Nicolai>> an email to HomotopyTypeTheory+unsub...@googlegroups.com

>> <mailto:HomotopyTypeTheory+unsub...@googlegroups.com>.

--

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 HomotopyTypeTheory+unsub...@googlegroups.com.

Oct 27, 2016, 1:12:50 PM10/27/16

to Homotopy Type Theory, homotopyt...@googlegroups.com, matthie...@inria.fr

This is (related to) Grothendieck's “inspiring assumption” of Pursuing Stacks section 28.

I only know of the treatment by Barwick and Schommer-Pries in On the Unicity of the Homotopy Theory of Higher Categories: https://arxiv.org/abs/1112.0040

Theorem 8.12 for n=0 says that the Kan complex of homotopy theories of (infinity,0)-categories is contractible. Of course this depends on their axiomatization, Definition 6.8. Perhaps some ideas can be adapted.

Cheers,

Ulrik

Oct 27, 2016, 3:44:43 PM10/27/16

to Ulrik Buchholtz, Homotopy Type Theory, matthie...@inria.fr

I think the earliest proof of some version of Grothendieck's

hypothèse inspiratrice is in the following paper of Cisinki.

http://www.tac.mta.ca/tac/volumes/20/17/20-17abs.html

It is my belief that Grothendieck's original formulation, which

was for the homotopy category itself (as opposed to a lifting of

it), is independent of ZFC. A proof of this would be fascinating.

I have occasionally speculated about trying to use HoTT to give

such an independence proof. Vladimir's comment suggests that one

direction of this is already done.

Best wishes,

Richard

hypothèse inspiratrice is in the following paper of Cisinki.

http://www.tac.mta.ca/tac/volumes/20/17/20-17abs.html

It is my belief that Grothendieck's original formulation, which

was for the homotopy category itself (as opposed to a lifting of

it), is independent of ZFC. A proof of this would be fascinating.

I have occasionally speculated about trying to use HoTT to give

such an independence proof. Vladimir's comment suggests that one

direction of this is already done.

Best wishes,

Richard

> --

> 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.
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

Oct 27, 2016, 4:18:31 PM10/27/16

to Homotopy Type Theory, homotopyt...@googlegroups.com, matthie...@inria.fr

Thanks all for the answer.

implied by univalence + some parametricity assumption ?".

Of course, assuming other axioms in the theory that allow to distinguish

between types makes it false.

Best,

On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau wrote:

Oct 27, 2016, 4:38:15 PM10/27/16

to Homotopy Type Theory, ulrikbu...@gmail.com, matthie...@inria.fr

Thanks, Richard!

Of course, this is not directly pertaining to Matthieu, Nicolas and Théo's question, but it's trying to capture an intuition that a universe should be rigid, at least when considered together with some structure.

How much structure suffices to make the universe rigid, and can we define this extra structure in HoTT? (We don't know how to say yet that the universe can be given the structure of an infinity-category strongly generated by 1, for example.)

Do you know other references that pertain to the inspiring assumption/hypothèse inspiratrice?

Best wishes,

Ulrik

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.

Oct 30, 2016, 4:57:00 PM10/30/16

to Ulrik Buchholtz, Homotopy Type Theory, matthie...@inria.fr

Hi Ulrik,

I mis-remembered the history a little: Corollary 5.2.2 of the

following paper of Toën and Vezzozi, from 2002, also gives a

proof of a lifting of the hypothèse inspiratrice.

https://arxiv.org/abs/math/0212330

As one would expect, the paper 'La théorie de l'homotopie de

Grothendieck' of Maltsiniotis also briefly discusses the original

hypothèse inspiratrice, early on in the introduction (see especially

the footnote).

I don't think that I know of other direct references beyond these,

except possibly in other writings of these authors; though the

quasi-categorical literature also, as one would expect, has a proof of

the same theorem as in the papers of Cisinski and Toën-Vezzosi.

I think that the Cisinski's paper gives a very clear reason to

expect the result to be true when formulated in the language of a

sufficiently rich 'homotopical category theory', whether the

language be that of derivators, (∞,1)-categories, or whatever.

It is remarkable that the result can be proven relatively easily

when formulated in a certain language, but if one insists on the

original version at the level of homotopy categories, then there seems

to be no way to approach it. This is the aspect of the hypothesis that

I am most interested in. A proof that the original hypothesis is

independent of ZFC would no doubt shed some very interesting light on

this dichotomy.

Best wishes,

Richard

> > an email to HomotopyTypeThe...@googlegroups.com <javascript:>.

I mis-remembered the history a little: Corollary 5.2.2 of the

following paper of Toën and Vezzozi, from 2002, also gives a

proof of a lifting of the hypothèse inspiratrice.

https://arxiv.org/abs/math/0212330

As one would expect, the paper 'La théorie de l'homotopie de

Grothendieck' of Maltsiniotis also briefly discusses the original

hypothèse inspiratrice, early on in the introduction (see especially

the footnote).

I don't think that I know of other direct references beyond these,

except possibly in other writings of these authors; though the

quasi-categorical literature also, as one would expect, has a proof of

the same theorem as in the papers of Cisinski and Toën-Vezzosi.

I think that the Cisinski's paper gives a very clear reason to

expect the result to be true when formulated in the language of a

sufficiently rich 'homotopical category theory', whether the

language be that of derivators, (∞,1)-categories, or whatever.

It is remarkable that the result can be proven relatively easily

when formulated in a certain language, but if one insists on the

original version at the level of homotopy categories, then there seems

to be no way to approach it. This is the aspect of the hypothesis that

I am most interested in. A proof that the original hypothesis is

independent of ZFC would no doubt shed some very interesting light on

this dichotomy.

Best wishes,

Richard

> --

> 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.
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

Oct 31, 2016, 6:00:59 AM10/31/16

to Richard Williamson, Ulrik Buchholtz, Homotopy Type Theory, matthie...@inria.fr

Just wanted to mention quickly for those who are interested in this kind of thing that a similar statement for the *stable* homotopy category is a theorem of Stefan Schwede's:

Eric

Oct 31, 2016, 9:07:54 AM10/31/16

to Homotopy Type Theory

Hello,

Some time in the last year or two, I saw a reference to a draft

paper which giving (roughly) a model for Martin-Loef type theory,

weakened so that judgemental equality was proof-relevant.

Unfortunately, I can't seem to find the message announcing the

draft, and was wondering if anyone here remembered it (perhaps

even because they wrote it).

Thanks for your help!

Best,

Neel

Some time in the last year or two, I saw a reference to a draft

paper which giving (roughly) a model for Martin-Loef type theory,

weakened so that judgemental equality was proof-relevant.

Unfortunately, I can't seem to find the message announcing the

draft, and was wondering if anyone here remembered it (perhaps

even because they wrote it).

Thanks for your help!

Best,

Neel

Oct 31, 2016, 5:43:16 PM10/31/16

to Neel Krishnaswami, Homotopy Type Theory

Are you thinking of

http://www.cs.ru.nl/~herman/PUBS/LambdaF.pdf

by any chance?

With kind regards,

Andrej

http://www.cs.ru.nl/~herman/PUBS/LambdaF.pdf

by any chance?

With kind regards,

Andrej

Oct 31, 2016, 6:01:58 PM10/31/16

to Andrej Bauer, Homotopy Type Theory

Hello,

No, the draft I was thinking of was a paper about the categorical

semantics of type theory.

However, this paper is quite relevant to my interests, as is (its

apparent successor) the LFMTP 2013 paper "Explicit Convertibility

Proofs in Pure Type Systems" by Floris van Doorn, Herman Geuvers and

Freek Wiedijk.

So in this sense my query has been unexpectedly successful. :)

Best,

Neel

No, the draft I was thinking of was a paper about the categorical

semantics of type theory.

However, this paper is quite relevant to my interests, as is (its

apparent successor) the LFMTP 2013 paper "Explicit Convertibility

Proofs in Pure Type Systems" by Floris van Doorn, Herman Geuvers and

Freek Wiedijk.

So in this sense my query has been unexpectedly successful. :)

Best,

Neel

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu