Just a small remark. 

It is indeed sui generis that equality in its various manifestations has 
this special status in type theory. 

It is not *just* that we have different notions of equality. The notions of 
equality play a fundamental role in the very **architecture** of type 
theories. 

The fundamental reason we need judgemental equality is, in particular, to 
make sense of type dependency. 

We can have a type theory with judgemental equality but without an identity 
type. 

It would be much more difficult, however, to have a type theory with an 
identity type but without a judgemental equality. (I am not saying it is 
impossible, and the idea sounds vaguely attractive.) 

Although HoTT/UF makes good sense of the identity type ("typal equality"), 
I am not convinced it gives the ultimate explanation of judgemental 
equality. (But I am listening.) 

Best, 
Martin 

On Monday, July 18, 2016 at 9:45:57 PM UTC+1, 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.
>
>