From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.66.154.165 with SMTP id vp5mr29560609pab.44.1468876659959; Mon, 18 Jul 2016 14:17:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.37.3 with SMTP id k3ls8323659otb.24.gmail; Mon, 18 Jul 2016 14:17:39 -0700 (PDT) X-Received: by 10.157.17.221 with SMTP id y29mr5808249oty.18.1468876659418; Mon, 18 Jul 2016 14:17:39 -0700 (PDT) Return-Path: Received: from out5-smtp.messagingengine.com (out5-smtp.messagingengine.com. [66.111.4.29]) by gmr-mx.google.com with ESMTPS id e189si1010524ith.3.2016.07.18.14.17.39 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Jul 2016 14:17:39 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.29 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) client-ip=66.111.4.29; Authentication-Results: gmr-mx.google.com; dkim=pass head...@messagingengine.com; spf=neutral (google.com: 66.111.4.29 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Received: from compute1.internal (compute1.nyi.internal [10.202.2.41]) by mailout.nyi.internal (Postfix) with ESMTP id C359920DDE for ; Mon, 18 Jul 2016 17:17:38 -0400 (EDT) Received: from web4 ([10.202.2.214]) by compute1.internal (MEProxy); Mon, 18 Jul 2016 17:17:38 -0400 DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-sasl-enc:x-sasl-enc; s=smtpout; bh=b6I0D7GpavKsWGy s7eX6EZYWMi4=; b=Neq691nfLGY/l8ohbtKfrSkJg+x5Dm3eV7HpYkGLhNHVdhy YZMulBSwiV6S9rA+dimbW4Or81LOIlYy9qU7PSlnoe68GGMD2ra0WoljCrUjKuXT 0zhcoYij1uj8euy2eRh2E6iyux7fQ0BITvU5HvhA+QdZdDKYrzSZbJ3lXs6M= Received: by mailuser.nyi.internal (Postfix, from userid 99) id 8CF64CC2C9; Mon, 18 Jul 2016 17:17:38 -0400 (EDT) Message-Id: <1468876658.2069095.669919241.7FD546F2@webmail.messagingengine.com> X-Sasl-Enc: f5quCmxfLkgrJzaGwYmQlt3RhcsQCWvQSDW1cTZ1WzeT 1468876658 From: Jon Sterling To: HomotopyTypeTheory@googlegroups.com MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" X-Mailer: MessagingEngine.com Webmail Interface - ajax-6fae4dd4 In-Reply-To: References: Subject: Re: [HoTT] Different notions of equality; terminology Date: Mon, 18 Jul 2016 14:17:38 -0700 > The effect of Martin-Lof's "propositional reflection rule" is simply to c= ollapse the two levels and make them one and the same. For the type theoris= t, this is really bad, because it breaks nice properties like normalization= 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 the= n not an "equality type", but something else=E2=80=94and figuring out precisely w= hat 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 thi= nk 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 whic= h 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. >=20 > One feature of type theory which is often confusing to newcomers is the= =20 > presence of several notions of equality. Today, at the opening of the=20 > FOMUS workshop, Vladimir gave a talk about the very subject -- but more > on=20 > that later. The two most common notions are usually called "definitional= =20 > equality" and "propositional equality". >=20 > It is agreed by most members of this list that the name of the latter=20 > notion is unfortunate, if not misleading. I would like to suggest the > name=20 > "logical equality" to be used for this notion. >=20 > First, let us summarize the two notions in greater detail. >=20 >=20 > 1. DEFINITIONAL EQUALITY. >=20 > PROPERTIES. >=20 > - Purely syntactic: "proofs" of this equality concern only the way the=20 > 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=20 > t.) > - Cannot be asserted in a derivation context [*] > - In total languages, is usually, but not always, decidable. >=20 > EXAMPLES. >=20 > - 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=20 > 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=20 > contextual equivalence). >=20 >=20 > 2. LOGICAL EQUALITY >=20 > 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; thus > - Allows a term of any type to be transported to a type logically equal > to=20 > it; > - May be interpreted weakly/as a path. >=20 > 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= =20 > Constructions); > - Extensional equality in Observational Type Theory; > - The Paths type in Cubical Type Theory. >=20 > The first example above is the main motivator for this terminological=20 > proposal. Whether one considers equality as a "logical symbol", it is=20 > obviously a concept which is present at the level of *formulas*. Under= =20 > formulae-as-types interpretation, one would naturally tend to think of it= =20 > as a proposition, until one came to realize that some types are not=20 > propositions. (Indeed, it was the only dependent type former in Howard's= =20 > original paper. Yet it could not be iterated/applied to itself.) >=20 > The point is that the second kind of equality is the one which can be=20 > reasoned about internally, *in the object logic*. Hence, it exists not > on=20 > the level of terms and definitions, but on the level of logic and=20 > proofs/constructions of formulae/types. >=20 >=20 > One argument against the adjective "logical" is that it can lead to=20 > confusion with "logical equivalence". But I don't think that that is a= =20 > certain outcome. >=20 > An alternative descriptor could be "type-level" or "type-theoretic", but= =20 > both are rather awkward and unrevealing. >=20 >=20 > Finally, Voevodsky currently distinguishes between "substitutive" and=20 > "transportational" equalities. But in his system, both concepts are of > the=20 > "logical" kind. The effect is therefore to promote "strict" equality to= =20 > the logical level; so one can reason about it in the object logic, while= =20 > retaining other properties like the conversion rule. >=20 > The effect of Martin-Lof's "propositional reflection rule" is simply to= =20 > collapse the two levels and make them one and the same. > For the type theorist, this is really bad, because it breaks nice=20 > properties like normalization and decidability of type checking. > For the homotopy type theorist, this is really bad, because it is=20 > inconsistent with univalence. >=20 > Best regards, > Andrew >=20 > [*] In certain settings, one can make sense of definitional equalities= =20 > "in-context" via the so-called Girard--Schroder-Heister (GSH) elimination= =20 > rule. >=20 > --=20 > 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.