From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.28.31.129 with SMTP id f123mr729631wmf.17.1477581554074;
        Thu, 27 Oct 2016 08:19:14 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.38.6 with SMTP id m6ls2751912wmm.3.canary-gmail; Thu, 27
 Oct 2016 08:19:13 -0700 (PDT)
X-Received: by 10.195.11.68 with SMTP id eg4mr698376wjd.17.1477581553433;
        Thu, 27 Oct 2016 08:19:13 -0700 (PDT)
Return-Path: <escardo...@googlemail.com>
Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150])
        by gmr-mx.google.com with ESMTPS id y7si317538wme.0.2016.10.27.08.19.13
        for <homotopyt...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Thu, 27 Oct 2016 08:19:13 -0700 (PDT)
Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150;
Authentication-Results: gmr-mx.google.com;
       spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com;
       dmarc=fail (p=QUARANTINE dis=QUARANTINE) header.from=googlemail.com
Received: from [147.188.128.127] (helo=bham.ac.uk)
	by sun61.bham.ac.uk with esmtp (Exim 4.84)
	(envelope-from <escardo...@googlemail.com>)
	id 1bzmSX-0005LG-Mb; Thu, 27 Oct 2016 16:19:13 +0100
Received: from mx1.cs.bham.ac.uk ([147.188.192.53])
	by bham.ac.uk (envelope-from
	<escardo...@googlemail.com>)
	with esmtp (Exim 4.84)
	id 1bzmSW-00011g-G0 
	using interface smart1.bham.ac.uk; Thu, 27 Oct 2016 16:19:12 +0100
Received: from dynamic200-118.cs.bham.ac.uk ([147.188.200.118])
	by mx1.cs.bham.ac.uk with esmtp (Exim 4.51)
	id 1bzmSW-0007K1-3M; Thu, 27 Oct 2016 16:19:12 +0100
Subject: Re: [HoTT] Is [Equiv Type_i Type_i] contractible?
To: Matthieu Sozeau <matthie...@inria.fr>,
 homotopytypetheory <homotopyt...@googlegroups.com>
References: <CALgtc7gp1VhjzF4h5GxpPCcsj0VUiGu4vuwQrrODDQU9u0jO+w@mail.gmail.com>
From: Martin Escardo <escardo...@googlemail.com>
Message-ID: <058585c6-426c-a0d7-f035-9dcc2d6cda61@googlemail.com>
Date: Thu, 27 Oct 2016 16:19:16 +0100
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101
 Thunderbird/45.3.0
MIME-Version: 1.0
In-Reply-To: <CALgtc7gp1VhjzF4h5GxpPCcsj0VUiGu4vuwQrrODDQU9u0jO+w@mail.gmail.com>
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
X-BHAM-SendViaRouter: yes

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.