From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.203.3 with SMTP id b3mr62607wmg.1.1468877079222; Mon, 18 Jul 2016 14:24:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.83.135 with SMTP id h129ls292293lfb.20.gmail; Mon, 18 Jul 2016 14:24:38 -0700 (PDT) X-Received: by 10.25.43.80 with SMTP id r77mr5727541lfr.4.1468877077976; Mon, 18 Jul 2016 14:24:37 -0700 (PDT) Return-Path: Received: from mail-lf0-x230.google.com (mail-lf0-x230.google.com. [2a00:1450:4010:c07::230]) by gmr-mx.google.com with ESMTPS id r74si741881wme.3.2016.07.18.14.24.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Jul 2016 14:24:37 -0700 (PDT) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::230 as permitted sender) client-ip=2a00:1450:4010:c07::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::230 as permitted sender) smtp.mailfrom=andrew....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x230.google.com with SMTP id g62so30697807lfe.3 for ; Mon, 18 Jul 2016 14:24:37 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=765Wimqvn7kNs0b3oJLknSfPKlXDwi/uR/hjQJqI7es=; b=IRSI1Y5a/PHbXBCcVTq32AtOlvJteEDj+SDHHQ2i0GMi0Tm4y4al6rjFUSiO/+RURa vXKc2YcVUkMctVeXCEQlJXmXW6bvGxdzhxidoJmhgacX2RHPnfxmDRMuFVSzREU2NFQC RDVvbOqtT/DaxGgjrhzaeZ8/CRcaQ7pe73FL+4Y1FhMtRvSqx9+s0ljKP8OpyKRN3OXY 0WvmajLxfkaDMM4tVwwBO6Mrh8pzeVOeHtK+JIxwoO00Urhuw9tGjVpllVIMTNEsGkST 2H2NKxqJMwAdyrNer6GF8g35U81hsAsnaBgYEcV2a28xLbyGGmuZMbCtxMkO7S5rvuT9 0lMg== X-Gm-Message-State: ALyK8tI9ESRojLvD0bg2iPShvcMZF0qP/AsZLLuVcAvengqKsjrDnIsivmytJjrgcG8kAqKfPmh0KFLEaslV7g== X-Received: by 10.25.24.233 with SMTP id 102mr14961073lfy.187.1468877077528; Mon, 18 Jul 2016 14:24:37 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.83.143 with HTTP; Mon, 18 Jul 2016 14:24:36 -0700 (PDT) In-Reply-To: <1468876658.2069095.669919241.7FD546F2@webmail.messagingengine.com> References: <1468876658.2069095.669919241.7FD546F2@webmail.messagingengine.com> From: Andrew Polonsky Date: Mon, 18 Jul 2016 23:24:36 +0200 Message-ID: Subject: Re: [HoTT] Different notions of equality; terminology To: Jon Sterling Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Dear Jon, I am sorry to have offended you, and I hope your advisor & heroes do not feel as you do. But I maintain, with humility, that propositional reflection is really, really bad. With respect, Andrew On Mon, Jul 18, 2016 at 11:17 PM, Jon Sterling wrot= e: >> The effect of Martin-Lof's "propositional reflection rule" is simply to = collapse the two levels and make them one and the same. For the type theori= st, this is really bad, because it breaks nice properties like normalizatio= n and decidability of type checking > > On the contrary, for a type theorist, this is *very good*. That's > because the entire type-theoretic/judgmental methodology is arranged > around a single move, which is to take a kind of observation which > exists at the judgmental level, and internalize it to one that exists at > the propositional level without losing information. > > So, "equality reflection" in MLTT is just the recognition that nothing > at all was added when the judgmental equality (which of course includes > all the standard laws from the meaning explanation, including functional > extensionality, etc.) was internalized into a proposition. > > It is interesting to remember that "equality reflection" is derivable > when restricted to the empty context (and, clearly, any type theory for > which this does not hold is broken=E2=80=94i.e. the type in question is t= hen not > an "equality type", but something else=E2=80=94and figuring out precisely= what > that "something else" is has been the main force of the past few years > in the development of cubical type theory). > > As you know, the concerns that you raise only come into play in the > rule's full generality at a non-empty context, which leads me to clarify > that the real "dangerous" force of equality reflection has little to do > with equality, and everything to do with the following position (which > you are free to accept or to reject depending on what you want to use > type theory for): > > The meaning of "G !- P true" (i.e. P under hypothesis) is completely > defined from the meaning of "G" and the meaning of "P" under no > hypotheses. > > Indeed, the standard semantics for type theory are arranged in this way. > Nonstandard semantics, including categories-with-families, follow the > approach pioneered in universal algebra, where the meaning of a type the > specification of its closed members, but rather specifies in addition > what its members shall be under an arbitrary context, subject of course > to various coherences with substitutions. > > Anyway, it's fine to want strong normalization (that is, normalization > in any context, even an inconsistent one!) & decidability=E2=80=94I can t= hink of > a million places where I *do* want this. But let's be precise and > collegial with our language instead of throwing around phrases like > "really bad"=E2=80=94there's no point to be insulting a body of theory wh= ich has > been incredibly successful and useful, and by extension, to insult & > dismiss the people who work on it, such as myself, my advisor, and many > of my friends and heroes. > > Thanks, > Jon > > On Mon, Jul 18, 2016, at 01:45 PM, Andrew Polonsky wrote: >> Good evening. >> >> One feature of type theory which is often confusing to newcomers is the >> presence of several notions of equality. Today, at the opening of the >> FOMUS workshop, Vladimir gave a talk about the very subject -- but more >> on >> that later. The two most common notions are usually called "definitiona= l >> equality" and "propositional equality". >> >> It is agreed by most members of this list that the name of the latter >> notion is unfortunate, if not misleading. I would like to suggest the >> name >> "logical equality" to be used for this notion. >> >> First, let us summarize the two notions in greater detail. >> >> >> 1. DEFINITIONAL EQUALITY. >> >> PROPERTIES. >> >> - Purely syntactic: "proofs" of this equality concern only the way the >> objects are presented; >> - Is always interpreted strictly; >> - Preserved under all contexts: >> If M=3DN definitionally, then C[M]=3DC[N], still definitionally; >> - Validates strict conversion rule: >> If t has type A, and A is definitionally equal to B, >> Then t *itself* has type B. (Not a transport of t, nor some term equal >> to >> t.) >> - Cannot be asserted in a derivation context [*] >> - In total languages, is usually, but not always, decidable. >> >> EXAMPLES. >> >> - Judgmental equality (in the LF formulation of type theory); >> - Untyped conversion (in the PTS formulation of type theory); >> - Well-typed conversion (all reduction subsequences must pass through >> well-typed terms); >> - Equalities which result from newly introduced rewrite rules; >> - Equalities which result from unification/pattern-matching constraints; >> - Any equalities arising from quotienting the term algebra (eg, by >> contextual equivalence). >> >> >> 2. LOGICAL EQUALITY >> >> PROPERTIES. >> - Is a type constructor/formula former in the object language; thus >> - Can be asserted into a derivation context; >> - Induces isomorphism/equivalence of fibers between dependent types; thu= s >> - Allows a term of any type to be transported to a type logically equal >> to >> it; >> - May be interpreted weakly/as a path. >> >> EXAMPLES. >> - The native equality of first-order logic; >> - In particular, equality in set theory; >> - Martin-Lof identity type; >> - Univalent equality in HoTT/UF; >> - Leibniz equality in impredicative dependent type theories (Calculus of >> Constructions); >> - Extensional equality in Observational Type Theory; >> - The Paths type in Cubical Type Theory. >> >> The first example above is the main motivator for this terminological >> proposal. Whether one considers equality as a "logical symbol", it is >> obviously a concept which is present at the level of *formulas*. Under >> formulae-as-types interpretation, one would naturally tend to think of i= t >> as a proposition, until one came to realize that some types are not >> propositions. (Indeed, it was the only dependent type former in Howard'= s >> original paper. Yet it could not be iterated/applied to itself.) >> >> The point is that the second kind of equality is the one which can be >> reasoned about internally, *in the object logic*. Hence, it exists not >> on >> the level of terms and definitions, but on the level of logic and >> proofs/constructions of formulae/types. >> >> >> One argument against the adjective "logical" is that it can lead to >> confusion with "logical equivalence". But I don't think that that is a >> certain outcome. >> >> An alternative descriptor could be "type-level" or "type-theoretic", but >> both are rather awkward and unrevealing. >> >> >> Finally, Voevodsky currently distinguishes between "substitutive" and >> "transportational" equalities. But in his system, both concepts are of >> the >> "logical" kind. The effect is therefore to promote "strict" equality to >> the logical level; so one can reason about it in the object logic, while >> retaining other properties like the conversion rule. >> >> The effect of Martin-Lof's "propositional reflection rule" is simply to >> collapse the two levels and make them one and the same. >> For the type theorist, this is really bad, because it breaks nice >> properties like normalization and decidability of type checking. >> For the homotopy type theorist, this is really bad, because it is >> inconsistent with univalence. >> >> Best regards, >> Andrew >> >> [*] In certain settings, one can make sense of definitional equalities >> "in-context" via the so-called Girard--Schroder-Heister (GSH) eliminatio= n >> rule. >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to a topic in the Go= ogle Groups "Homotopy Type Theory" group. > To unsubscribe from this topic, visit https://groups.google.com/d/topic/H= omotopyTypeTheory/1bUtH8CLGQg/unsubscribe. > To unsubscribe from this group and all its topics, send an email to Homot= opyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.