Different notions of equality; terminology

[Andrew Polonsky <andrew....@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 4214 bytes --]

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.


[-- Attachment #1.2: Type: text/html, Size: 5195 bytes --]