From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.38.144 with SMTP id l16mr29899754otb.24.1468880654336; Mon, 18 Jul 2016 15:24:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.19.150 with SMTP id 22ls3445830iot.17.gmail; Mon, 18 Jul 2016 15:24:13 -0700 (PDT) X-Received: by 10.66.135.20 with SMTP id po20mr29279568pab.2.1468880653164; Mon, 18 Jul 2016 15:24:13 -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 f206si597306ywb.6.2016.07.18.15.24.12 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Jul 2016 15:24:13 -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 compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id E883421212 for ; Mon, 18 Jul 2016 18:24:11 -0400 (EDT) Received: from web4 ([10.202.2.214]) by compute2.internal (MEProxy); Mon, 18 Jul 2016 18:24:11 -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=w1FlOSXEXAdyUMx g9eaehrfGLxY=; b=l2RFekfjTMOp+isnCLFgkZzPJOOOTlH4mlruwnYM3tnAaXo wiNDB9bq7uEFwXOJ+gfJg3L9Twr1ny9/bFolbHr0uo35DGwKIldHoIgDxHGmUzqm 49sMhjy/epAAAAi3SjbV4zKD4MvGz9uRjtd7d8yjonjssnB0TzKnOKWRvO6s= Received: by mailuser.nyi.internal (Postfix, from userid 99) id AFC49CC2C9; Mon, 18 Jul 2016 18:24:11 -0400 (EDT) Message-Id: <1468880651.2082774.669987137.6097A3A2@webmail.messagingengine.com> X-Sasl-Enc: KQ2lemDGY86e7Rwtlni6/4PA9HfoQfxMuoYg23DE9ejj 1468880651 From: Jon Sterling To: HomotopyTypeTheory@googlegroups.com MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="ISO-8859-1" 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 15:24:11 -0700 On Mon, Jul 18, 2016, at 03:20 PM, Andrew Polonsky wrote: > That may all be true. >=20 > Yet, -- in this particular case -- it may actually be a good idea NOT > to depart completely from the traditional, intuitive meaning of > "logical". >=20 > The point is that here we are talking about what is really the most > elementary, the most canonical, the most ancient concept of equality. > The adjective "typal" suggests that something new happened when we > transitioned from FOL to MLTT. But that change, whatever you call it, > (higher-dimensionality?) -- it affected equality in the same way as > all other formulae. >=20 > So it is not a new concept. It is the same concept. >=20 > Regarding "judgmental" equality, this is a special case of > definitional equality. Some formulations of type theory have it, > others don't. >=20 > For example type theories implemented in the Coq and Agda proof > assistants, they do not have judgmental equality. In PTS formulations > of type theory, definitional equality is not a judgment. This is false, as far as I am aware. From what Peter Dybjer told me, Agda is based on an extension of Martin-L=F6f's Logical Framework + Monomorphic Theory of Sets (these are described in "Programming in Martin-L=F6f's Type Theory"). Now, there's some differences between Agda's type theory and MLLF+MTS, but both absolutely have judgmental equality. I am not familiar enough with Coq's type theory to comment on it. Kind regards, Jon >=20 > Cheers, > Andrew >=20 > On Tue, Jul 19, 2016 at 12:02 AM, Michael Shulman > wrote: > > I have been advocating the term "typal equality" for what used to be > > called "propositional". It is less awkward than "type-level" or > > "type-theoretic", and conveys exactly what is meant, namely that the > > statement of equality *is a type*. I prefer it to "logical equality" > > because traditionally, "logic" has often referred only to the type > > theory of mere propositions, so "logical equality" has something of > > the same problem as "propositional equality". > > > > (For the same reasons I prefer "judgmental equality" because it > > conveys exactly what is meant in that case, namely that the statement > > of equality *is a judgment*. Sometimes it is accurate to call it > > "definitional equality", but it is not always the case that such a > > statement of equality *is a definition*.) > > > > On Mon, Jul 18, 2016 at 5:45 PM, Andrew Polonsky > > wrote: > >> Good evening. > >> > >> One feature of type theory which is often confusing to newcomers is th= e > >> 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 t= hat > >> later. The two most common notions are usually called "definitional > >> 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 equ= al 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 constraint= s; > >> - 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; t= hus > >> - Allows a term of any type to be transported to a type logically equa= l 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*. Unde= r > >> formulae-as-types interpretation, one would naturally tend to think of= it as > >> a proposition, until one came to realize that some types are not > >> propositions. (Indeed, it was the only dependent type former in Howar= d'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 no= t 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", b= ut > >> both are rather awkward and unrevealing. > >> > >> > >> Finally, Voevodsky currently distinguishes between "substitutive" and > >> "transportational" equalities. But in his system, both concepts are o= f 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 t= o > >> collapse the two levels and make them one and the same. > >> For the type theorist, this is really bad, because it breaks nice prop= erties > >> 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 equalitie= s > >> "in-context" via the so-called Girard--Schroder-Heister (GSH) eliminat= ion > >> rule. > >> > >> -- > >> You received this message because you are subscribed to the Google Gro= ups > >> "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. >=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.