Re: [HoTT] Different notions of equality; terminology

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

> case I think it better to use a word that conveys *exactly* what the
> distinction is,

The distinction is that it is the equality
predicate/formula/thing-you-can-prove-or-inhabit.

> I suppose judgmental equality doesn't have to be formulated as a
> judgment, but as far as I know in all cases it can be so, without
> changing the type theory materially.

In principle, this should of course always be possible.  But in
practice, one often describes and implements the systems long before
the conjecture above is verified. (If ever.)

>  It is not always, however, a
> definition; for instance, in type theory with a reflection rule from
> typal equality to judgmental, there is no sense in which a judgmental
> equality obtained by that rule is a "definition" of one side in terms
> of the other.

In type theory with reflection rule, one can think of all equalities
as "definitional", including those that appear in the hypothesis of
the reflection rule.

Andrew