From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 18 Jul 2016 13:45:56 -0700 (PDT) From: Andrew Polonsky To: Homotopy Type Theory Message-Id: Subject: Different notions of equality; terminology MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_734_13028554.1468874756664" ------=_Part_734_13028554.1468874756664 Content-Type: multipart/alternative; boundary="----=_Part_735_261135666.1468874756664" ------=_Part_735_261135666.1468874756664 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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. ------=_Part_735_261135666.1468874756664 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Good evening.

One feature of= type theory which is often confusing to newcomers is the presence of sever= al notions of equality. =C2=A0Today, at the opening of the FOMUS workshop, = Vladimir gave a talk about the very subject -- but more on that later. =C2= =A0The two most common notions are usually called "definitional equali= ty" and "propositional equality".

I= t is agreed by most members of this list that the name of the latter notion= is unfortunate, if not misleading. =C2=A0I 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: "proof= s" of this equality concern only the way the objects are presented;
- Is always interpreted strictly;
- Preserved under all c= ontexts:
=C2=A0 If M=3DN definitionally, then C[M]=3DC[N], still = definitionally;
- Validates strict conversion rule:
=C2= =A0 If t has type A, and A is definitionally equal to B,
=C2=A0 T= hen 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 for= mulation of type theory);
- Well-typed conversion (all reduction = subsequences must pass through well-typed terms);
- Equalities wh= ich result from newly introduced rewrite rules;
- Equalities whic= h result from unification/pattern-matching constraints;
- Any equ= alities arising from quotienting the term algebra (eg, by contextual equiva= lence).


2. LOGICAL EQUALITY

PROPERTIES.
- Is a type constructor/formula for= mer in the object language; thus
- Can be asserted into a derivat= ion context;
- Induces isomorphism/equivalence of fibers between = dependent types; thus
- Allows a term of any type to be transport= ed to a type logically equal to it;
- May be interpreted weakly/a= s a path.

EXAMPLES.
- The native equalit= y of first-order logic;
- In particular, equality in set theory;<= /div>
- Martin-Lof identity type;
- Univalent equality in HoT= T/UF;
- Leibniz equality in impredicative dependent type theories= (Calculus of Constructions);
- Extensional equality in Observati= onal Type Theory;
- The Paths type in Cubical Type Theory.
<= div>
The first example above is the main motivator for this t= erminological proposal. =C2=A0Whether one considers equality as a "log= ical symbol", it is obviously a concept which is present at the level = of *formulas*. =C2=A0Under formulae-as-types interpretation, one would natu= rally tend to think of it as a proposition, until one came to realize that = some types are not propositions. =C2=A0(Indeed, it was the only dependent t= ype former in Howard's original paper. =C2=A0Yet it could not be iterat= ed/applied to itself.)

The point is that the secon= d kind of equality is the one which can be reasoned about internally, *in t= he object logic*. =C2=A0Hence, it exists not on the level of terms and defi= nitions, but on the level of logic and proofs/constructions of formulae/typ= es.


One argument against the adject= ive "logical" is that it can lead to confusion with "logical= equivalence". =C2=A0But I don't think that that is a certain outc= ome.

An alternative descriptor could be "type= -level" or "type-theoretic", but both are rather awkward and= unrevealing.


Finally, Voevodsky cu= rrently distinguishes between "substitutive" and "transporta= tional" equalities. =C2=A0But in his system, both concepts are of the = "logical" kind. =C2=A0The effect is therefore to promote "st= rict" 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 on= e and the same.
For the type theorist, this is really bad, becaus= e it breaks nice properties like normalization and decidability of type che= cking.
For the homotopy type theorist, this is really bad, becaus= e it is inconsistent with univalence.

Best regards= ,
Andrew

[*] =C2=A0In certain settings, = one can make sense of definitional equalities "in-context" via th= e so-called Girard--Schroder-Heister (GSH) elimination rule.

=
------=_Part_735_261135666.1468874756664-- ------=_Part_734_13028554.1468874756664--