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.