From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.153.211 with SMTP id b202mr4005410lfe.0.1468880461953; Mon, 18 Jul 2016 15:21:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.176.66 with SMTP id z63ls859642wme.10.canary; Mon, 18 Jul 2016 15:21:01 -0700 (PDT) X-Received: by 10.194.95.133 with SMTP id dk5mr589001wjb.4.1468880461128; Mon, 18 Jul 2016 15:21:01 -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 o10si841300wme.0.2016.07.18.15.21.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Jul 2016 15:21:01 -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 b199so384893lfe.0 for ; Mon, 18 Jul 2016 15:21:01 -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; bh=lWKfT+8JiVs9mS3RLGYyMQ8CfUWmocRXAsWlpZAbjZg=; b=SmyOwVtzkzIMIisZ694tv1Anh4j3cYM2IjJwUi+BNFPp6pYwexllN8j4VAwqwJTOQF hX/T2eCIywN6DVrk4w+VAGnC/kmjngyW7YEmPKdFc8W+UzzwZONf+fWViZ7OlwLDsUZL PfIJakaTz8sQJma+NGoA6RzOPq6BNConXZST3Mm5uZKxeRBEasIw4Q5FZgpmBC0lZUyh qBnl+zpYJZ2uu7QmXvdONOmqlAFGpwkHvIkSIvFBamo+1LhGZTXIHQFY9fE5KnuwiBkq MV0AJKlxLpLA3RwiAqM2pKgAnpihb0KOSQ9q5DlxOrCsEdpcWTiiuZCjiG+Fw/c7H9cm +SRQ== X-Gm-Message-State: ALyK8tJNB5ocTawoFQwnpv4a8GgshKMRQNSi4QqHlORDan1/Yv6yQPDPgL3li2w7ZXvbEj/kec+8wq9kcTS6kw== X-Received: by 10.25.217.151 with SMTP id s23mr16666490lfi.16.1468880460496; Mon, 18 Jul 2016 15:21:00 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.83.143 with HTTP; Mon, 18 Jul 2016 15:20:59 -0700 (PDT) In-Reply-To: References: From: Andrew Polonsky Date: Tue, 19 Jul 2016 00:20:59 +0200 Message-ID: Subject: Re: [HoTT] Different notions of equality; terminology To: Michael Shulman Cc: Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 That may all be true. Yet, -- in this particular case -- it may actually be a good idea NOT to depart completely from the traditional, intuitive meaning of "logical". 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. So it is not a new concept. It is the same concept. Regarding "judgmental" equality, this is a special case of definitional equality. Some formulations of type theory have it, others don't. 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. Cheers, Andrew 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 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 "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=N definitionally, then C[M]=C[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; thus >> - 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 it 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) elimination >> rule. >> >> -- >> 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.