From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.33.96 with SMTP id h93mr2047365ljh.4.1473632766965; Sun, 11 Sep 2016 15:26:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.137.4 with SMTP id l4ls1090234wmd.26.gmail; Sun, 11 Sep 2016 15:26:06 -0700 (PDT) X-Received: by 10.28.207.131 with SMTP id f125mr1154060wmg.4.1473632766365; Sun, 11 Sep 2016 15:26:06 -0700 (PDT) Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id e21si678557wmc.2.2016.09.11.15.26.06 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 11 Sep 2016 15:26:06 -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 ) id 1bjDCQ-0000Yx-N8 for HomotopyT...@googlegroups.com; Sun, 11 Sep 2016 23:26:06 +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 ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1bjDCQ-0006im-DD for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Sun, 11 Sep 2016 23:26:06 +0100 Subject: Re: [HoTT] Meta-conjecture about MLTT References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> To: "HomotopyT...@googlegroups.com" From: Martin Escardo Message-ID: <794290b0-7730-b014-a144-a79ef682e5aa@googlemail.com> Date: Sun, 11 Sep 2016 23:26:05 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) Nice. Would you agree with the following imprecise understanding of your construction: Given any interpretation of the theory, any type can be substituted by an isomorphic copy to again get an interpretation, (even) in the presence of equality reflection. Or is more going on in your construction? Martin Martin En 11/09/16 23:08, Peter LeFanu Lumsdaine wrote: > As you conjecture, MLTT with equality reflection can’t distinguish > between isomorphic types. > > Precisely, let MLTT[X] be the extension of MLTT by a single closed base > type X. > > Suppose \C is a model of MLTT — presented as a CwA with appropriate > extra logical structure — and A, B are two isomorphic types in it, over > the empty context. So A, B induce two interpretations of MLTT[X] in \C. > > Then there’s a CwA \C^\iso, with the category of isomorphisms in \C, and > with a type over an iso Г1 <~> Г2 being a pair of types A1, A2 over Г1, > Г2 that correspond under reindexing along the isomorphism. > > Now I claim this carries suitable structure to again model MLTT[X], and > furthermore (importantly) such that the two projection maps \C^\iso —> > \C both preserve all the logical structure. For most logical > type-formers (Pi’s, Sigma’s, etc), the structure is by showing that > these type-formers are provably functorial in isomorphisms. (This uses > the equality reflection.) For the universe(s), this just uses the > identity iso on the universe(s) of \C. The base type X, we model by the > given isomorphism A <~> B. > > So this induces an interpretation of MLTT[X] in \C^\iso, whose two > projections to \C are the two original interpretations in \C. > > In particular, if P is any type in MLTT[X] — i.e. a property of an > arbitrary type definable in MLTT — then its interpretation in \C^\iso is > an isomorphism P[A] <~> P[B]. I think this is a reasonable positive > answer to your question? > > I don’t remember anywhere this construction appears in the literature, > but I’ve always assumed that it has been noted before. (Actually, I’d > be very glad to hear a reference if anyone remembers seeing this > somewhere, even if only in folklore not in print.) Without identity > reflection, it no longer works — since one doesn’t know that the logical > structure in \C respects isomorphisms between types — but essentially > the same approach works once one replaces isomorphisms by equivalences. > This is in the work of Chris Kapulkin’s and mine that I presented in > Bonn in February, which we hope to have written up very soon… > > Best, > –Peter. > > > On Sun, Sep 11, 2016 at 10:47 PM, 'Martin Escardo' via Homotopy Type > Theory > wrote: > > 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 > > > -- > 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 > . > >