Is [Equiv Type_i Type_i] contractible?

Is [Equiv Type_i Type_i] contractible?

[Matthieu Sozeau]

[-- Attachment #1: Type: text/plain, Size: 516 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 1232 bytes --]

Re: [HoTT] Is [Equiv Type_i Type_i] contractible?

[Martin Escardo]

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

On 27/10/16 16:15, Matthieu Sozeau wrote:
> 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
> 
> -- 
> 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.

Re: [HoTT] Is [Equiv Type_i Type_i] contractible?

[Martin Escardo]

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. But here is one proof which is
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.)

I can find this one, which is slightly more complicated, but still short:

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

Martin



> 
> Hence "potentially" there are at least two automorphisms of U.
> 
> Martin
> 
> On 27/10/16 16:15, Matthieu Sozeau wrote:
>> 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
>>
>> -- 
>> 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.
> 

Re: [HoTT] Is [Equiv Type_i Type_i] contractible?

[Nicolai Kraus]

[-- Attachment #1: Type: text/plain, Size: 2728 bytes --]

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



> But here is one proof which is
> 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.)
>
> I can find this one, which is slightly more complicated, but still short:
>
> https://groups.google.com/d/msg/homotopytypetheory/
> 8CV0S2DuOI8/Jn5EeSwxc4gJ
>
> Martin
>
>
>
> >
> > Hence "potentially" there are at least two automorphisms of U.
> >
> > Martin
> >
> > On 27/10/16 16:15, Matthieu Sozeau wrote:
> >> 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
> >>
> >> --
> >> 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.
> >
>
> --
> 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.
>

[-- Attachment #2: Type: text/html, Size: 4381 bytes --]

Re: [HoTT] Is [Equiv Type_i Type_i] contractible?

[Vladimir Voevodsky]

[-- Attachment #1: Type: text/plain, Size: 1358 bytes --]

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.

> On Oct 27, 2016, at 11:15 AM, Matthieu Sozeau <matthie...@inria.fr> wrote:
> 
> 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
> 
> -- 
> 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 <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 2790 bytes --]

Re: Is [Equiv Type_i Type_i] contractible?

[Ulrik Buchholtz]

[-- Attachment #1.1: Type: text/plain, Size: 1119 bytes --]

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

On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau wrote:
>
> 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
>

[-- Attachment #1.2: Type: text/html, Size: 1952 bytes --]

Re: [HoTT] Re: Is [Equiv Type_i Type_i] contractible?

[Richard Williamson]

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

On Thu, Oct 27, 2016 at 10:12:50AM -0700, Ulrik Buchholtz wrote:
> 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
>
> On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau wrote:
> >
> > 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
> >
>
> --
> 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.

Re: [HoTT] Re: Is [Equiv Type_i Type_i] contractible?

[Ulrik Buchholtz]

[-- Attachment #1.1: Type: text/plain, Size: 2992 bytes --]

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

On Thursday, October 27, 2016 at 9:44:43 PM UTC+2, Richard Williamson wrote:
>
> 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 
>
> On Thu, Oct 27, 2016 at 10:12:50AM -0700, Ulrik Buchholtz wrote: 
> > 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 
> > 
> > On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau 
> wrote: 
> > > 
> > > 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 
> > > 
> > 
> > -- 
> > 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 <javascript:>. 
>
> > For more options, visit https://groups.google.com/d/optout. 
>
>

[-- Attachment #1.2: Type: text/html, Size: 5328 bytes --]

Re: [HoTT] Re: Is [Equiv Type_i Type_i] contractible?

[Richard Williamson]

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

On Thu, Oct 27, 2016 at 01:38:15PM -0700, Ulrik Buchholtz wrote:
> 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
>
> On Thursday, October 27, 2016 at 9:44:43 PM UTC+2, Richard Williamson wrote:
> >
> > 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
> >
> > On Thu, Oct 27, 2016 at 10:12:50AM -0700, Ulrik Buchholtz wrote:
> > > 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
> > >
> > > On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau
> > wrote:
> > > >
> > > > 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
> > > >
> > >
> > > --
> > > 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 <javascript:>.
> >
> > > For more options, visit https://groups.google.com/d/optout.
> >
> >
>
> --
> 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.

Re: [HoTT] Re: Is [Equiv Type_i Type_i] contractible?

[Eric Finster]

[-- Attachment #1: Type: text/plain, Size: 5810 bytes --]

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:

http://www.math.uni-bonn.de/people/schwede/rigid.pdf

Eric


On Sun, Oct 30, 2016 at 9:57 PM Richard Williamson <rwilli...@gmail.com>
wrote:

> 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
>
> On Thu, Oct 27, 2016 at 01:38:15PM -0700, Ulrik Buchholtz wrote:
> > 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
> >
> > On Thursday, October 27, 2016 at 9:44:43 PM UTC+2, Richard Williamson
> wrote:
> > >
> > > 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
> > >
> > > On Thu, Oct 27, 2016 at 10:12:50AM -0700, Ulrik Buchholtz wrote:
> > > > 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
> > > >
> > > > On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau
> > > wrote:
> > > > >
> > > > > 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
> > > > >
> > > >
> > > > --
> > > > 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
> <javascript:>.
> > >
> > > > For more options, visit https://groups.google.com/d/optout.
> > >
> > >
> >
> > --
> > 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.
>
> --
> 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.
>

[-- Attachment #2: Type: text/html, Size: 10181 bytes --]

MLTT with proof-relevant judgmental equality?

[Neel Krishnaswami]

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

Re: [HoTT] MLTT with proof-relevant judgmental equality?

[Andrej Bauer]

Are you thinking of

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

by any chance?

With kind regards,

Andrej

Re: [HoTT] MLTT with proof-relevant judgmental equality?

[Neel Krishnaswami]

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



On 31/10/16 21:43, Andrej Bauer wrote:
> Are you thinking of
>
> http://www.cs.ru.nl/~herman/PUBS/LambdaF.pdf
>
> by any chance?
>
> With kind regards,
>
> Andrej
>

Re: Is [Equiv Type_i Type_i] contractible?

[nicolas tabareau]

[-- Attachment #1.1: Type: text/plain, Size: 900 bytes --]

Thanks all for the answer.

I think our question was more "is it compatible with univalence or 
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:
>
> 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
>

[-- Attachment #1.2: Type: text/html, Size: 1742 bytes --]