From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.46.32.76 with SMTP id g73mr2009008ljg.9.1473626858682;
        Sun, 11 Sep 2016 13:47:38 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.166.146 with SMTP id p140ls1052797wme.21.canary; Sun, 11
 Sep 2016 13:47:38 -0700 (PDT)
X-Received: by 10.194.96.237 with SMTP id dv13mr315220wjb.6.1473626858034;
        Sun, 11 Sep 2016 13:47:38 -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 p199si864650wmd.1.2016.09.11.13.47.37
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Sun, 11 Sep 2016 13:47:38 -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.54] (helo=mailer3)
	by sun61.bham.ac.uk with esmtp (Exim 4.84)
	(envelope-from <escardo...@googlemail.com>)
	id 1bjBf7-0001pv-P7
	for HomotopyT...@googlegroups.com; Sun, 11 Sep 2016 21:47:37 +0100
Received: from host86-137-209-253.range86-137.btcentralplus.com ([86.137.209.253] helo=[192.168.1.112])
	by bham.ac.uk (envelope-from
	<escardo...@googlemail.com>)
	with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128)
	(Exim 4.84)
	id 1bjBf7-0002T6-FD
	for HomotopyT...@googlegroups.com 
	using interface auth-smtp.bham.ac.uk; Sun, 11 Sep 2016 21:47:37 +0100
To: "HomotopyT...@googlegroups.com"
 <HomotopyT...@googlegroups.com>
From: Martin Escardo <escardo...@googlemail.com>
Subject: Meta-conjecture about MLTT
Message-ID: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com>
Date: Sun, 11 Sep 2016 21:47:36 +0100
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101
 Thunderbird/45.2.0
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
X-BHAM-SendViaRouter: yes
X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom)

In MLTT with equality reflection, we cannot distinguish isomorphic types.

There was some agreement regarding this in previous discussions here in 
this list in the past (I think).

But I don't think we actually saw a proof (have we?). As far as I 
understand, we only saw that natural attempts to distinguish examples of 
isomorphic types fail. There was some invokation of realizability models 
to try to justify this. But I am not (yet) convinced by the arguments I 
have seen so far.

Nevertheless, I am convinced that equality reflection in MLTT cannot be 
used to distinguish any particular pair of isomorphic types. (Prove me 
wrong.)

The meta-task is to either produce two isomorphic types in an empty 
context, together with a property that one of them provably has but the 
other doesn't, or to show that this is impossible.

I am strongly inclined to think that this is impossible: that so-called 
extensional MLTT cannot distinguish isomorphic types.

In particular, equality-reflection has nothing whatsoever to do 5with 
elementwise equality.

Of course, what makes this difficult is that MLTT with equality 
reflection is inconsistent with univalence.


Martin