From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.168.193 with SMTP id r184mr309191wme.1.1473325895323; Thu, 08 Sep 2016 02:11:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.44.203 with SMTP id s194ls77552lfs.32.gmail; Thu, 08 Sep 2016 02:11:34 -0700 (PDT) X-Received: by 10.46.5.140 with SMTP id 134mr498278ljf.6.1473325894655; Thu, 08 Sep 2016 02:11:34 -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 a126si488134wmd.1.2016.09.08.02.11.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Sep 2016 02:11:34 -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 ) id 1bhvMs-000559-Np for HomotopyT...@googlegroups.com; Thu, 08 Sep 2016 10:11:34 +0100 Received: from mx1.cs.bham.ac.uk ([147.188.192.53]) by bham.ac.uk (envelope-from ) with esmtp (Exim 4.84) id 1bhvMs-00034E-E0 for HomotopyT...@googlegroups.com using interface smart1.bham.ac.uk; Thu, 08 Sep 2016 10:11:34 +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 1bhvMs-0004UR-7y for HomotopyT...@googlegroups.com; Thu, 08 Sep 2016 10:11:34 +0100 Subject: Re: [HoTT] A puzzle about "univalent equality" References: <876efd6d-5c0b-488d-a72a-0a2d14ecb0ec@googlegroups.com> <9064B371-C3B0-45F5-8720-90E6D10E211C@cs.cmu.edu> <143ade6b-1b68-36fe-a765-c54d9f6fac8c@googlemail.com> To: Homotopy Type Theory From: Martin Escardo Message-ID: <8219d98e-0032-c6df-cb21-d864f86c885f@googlemail.com> Date: Thu, 8 Sep 2016 10:11:36 +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 Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes On 08/09/16 07:06, Jason Gross wrote: >> Can we stare at the type (Id U X Y) >> objectively, mathematically, say >> within intensional MLTT, where it was >> introduced, and, internally in >> MLTT, ponder what it can be, and identify the >> only "compelling" thing it >> can be as the type of equivalences X~Y, >> where "compelling" is a notion >> remote from univalence? > > I am not sure what you mean by internally, but the way I usually > motivate univalence is: we can ask "which equalities (Id U X Y) are > provable in MLTT?" The answer is: "only when X and Y are definitionally > equal." We can ask: "when can we prove that (Id U X Y) is absurd?" The > answer turns out to be: "exactly when X and Y are provably not > isomorphic." (The proof that this is the most general answer is the > proof that univalence is consistent.) So it seems natural to ask about > the two extremes. On the one hand, the converse of the strictest > equality we can have is the equality reflection rule. On the other > extreme, the inverse of the weakest equality rule is logically > equivalent to univalence. Ok, I would regard this as an external, experimental motivation. I use a similar one (and so do other people): (intensional or extensional) MLTT cannot distinguish isomorphic types by exhibiting a property that one (provably) has but not the other. For intensional MLTT the proof is the consistency of univalence. For extensional MLTT this can be proved via realizability models (we discussed this in this list, I think). So this is a weak justification for univalence, because extensional MLTT already has this meta-theoretical property, but is not consistent with univalence. In any case, this is a meta-level statement, and I was looking more something internal. Because I am looking for something internal, equality reflection doesn't qualify (as it cannot be taken as a hypothesis, as it is not a type but a rule). The K axiom does qualify as something that one can hypothesize internally, as does univalence. In November last year, I observed in this list thatI, in MLTT, we can construct a map E: {X Y : U} -> (X->Y) -> U and a (recursively defined) equivalence Phi: {X Y : U} -> X=Y -> Sigma(f:X->Y).E(f). Because this is in intensional MLTT, it is also a theorem/construction of extensional MLTT, with equality-reflection present but not used. We have that E(f) -> isEquiv(f). The K axiom (which holds in the presence of equality reflection) is of course equivalent to saying that the only E-map X->X is the identity. In the other extreme, univalence is the converse implication E(f) <- isEquiv(f), saying that all equivalences X->Y are E-maps. But can we "locate" univalence among the space of possibilities for E other than saying that it is one of the two extreme possibilities? Martin > > On Wed, Sep 7, 2016, 9:15 PM Michael Shulman > wrote: > > Does "Zermelo-style set-theoretic equality" even make sense in MLTT? > Types don't have the global membership structure that Zermelo-sets do. > > On Wed, Sep 7, 2016 at 4:18 PM, Matt Oliveri > wrote: > > On Tuesday, September 6, 2016 at 6:14:24 PM UTC-4, Martin Hotzel > Escardo > > wrote: > >> > >> Some people like the K-axiom for U because ... (let them fill the > answer). > > > > > > It allows you to interpret (within type theory) the types of ITT + > K as > > types of U, and their elements as the corresponding elements. > (Conjecture?) > > Whereas without K, we don't know how to interpret ITT types as > types of U. > > In other words, K is a simple way to give ITT reflection. > > > >> Can we stare at the type (Id U X Y) objectively, mathematically, say > >> within intensional MLTT, where it was introduced, and, internally in > >> MLTT, ponder what it can be, and identify the only "compelling" > thing it > >> can be as the type of equivalences X~Y, where "compelling" is a > notion > >> remote from univalence? > > > > > > How does Zermelo-style set-theoretic equality get ruled out as a > potential > > "compelling" meaning for identity? Of course, there's a potential > argument > > about what "compelling" ought to be getting at. You seem to not > consider > > set-theoretic equality compelling, which I can play along with. > > > > -- > > 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. > > -- > 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.