From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 27 Oct 2016 13:18:30 -0700 (PDT) From: nicolas tabareau To: Homotopy Type Theory Cc: homotopyt...@googlegroups.com, matthie...@inria.fr Message-Id: <8564e3b5-1226-404e-a6ed-716c5519cdb0@googlegroups.com> In-Reply-To: References: Subject: Re: Is [Equiv Type_i Type_i] contractible? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_435_1928491977.1477599510832" ------=_Part_435_1928491977.1477599510832 Content-Type: multipart/alternative; boundary="----=_Part_436_133166480.1477599510832" ------=_Part_436_133166480.1477599510832 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Thanks all for the answer. I think our question was more "is it compatible with univalence or=20 implied by univalence + some parametricity assumption ?". Of course, assuming other axioms in the theory that allow to distinguish between types makes it false. Best,=20 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=C3=A9o Winterhalte= r on=20 > the above question. Is it the case that all equivalences between a univer= se=20 > and itself are equivalent to the identity? We can't seem to prove (or=20 > disprove) this from univalence alone, and even additional parametricity= =20 > assumptions do not seem to help. Did we miss a counterexample? Did anyone= =20 > investigate this or can produce a proof as an easy corollary? What is the= =20 > situation in, e.g. the simplicial model? > > -- Matthieu > ------=_Part_436_133166480.1477599510832 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Thanks all for the answer.

I thin= k our question was more "is it compatible with univalence or=C2=A0implied by univalence + some parametricity assumption ?".
<= br>
Of course, assuming other axioms in the theory that allow to = distinguish
between types makes it false.

Best,=C2=A0

On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Mat= thieu Sozeau wrote:
Dear all,

=C2=A0 we've been stuck with N. Tabareau and his student Th=C3= =A9o Winterhalter on the above question. Is it the case that all equivalenc= es between a universe and itself are equivalent to the identity? We can'= ;t seem to prove (or disprove) this from univalence alone, and even additio= nal parametricity assumptions do not seem to help. Did we miss a counterexa= mple? Did anyone investigate this or can produce a proof as an easy corolla= ry? What is the situation in, e.g. the simplicial model?

-- Matthieu
------=_Part_436_133166480.1477599510832-- ------=_Part_435_1928491977.1477599510832--