Re: [HoTT] Different notions of equality; terminology

[Jon Sterling <j...@jonmsterling.com>]

> 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

On the contrary, for a type theorist, this is *very good*. That's
because the entire type-theoretic/judgmental methodology is arranged
around a single move, which is to take a kind of observation which
exists at the judgmental level, and internalize it to one that exists at
the propositional level without losing information.

So, "equality reflection" in MLTT is just the recognition that nothing
at all was added when the judgmental equality (which of course includes
all the standard laws from the meaning explanation, including functional
extensionality, etc.) was internalized into a proposition.

It is interesting to remember that "equality reflection" is derivable
when restricted to the empty context (and, clearly, any type theory for
which this does not hold is broken—i.e. the type in question is then not
an "equality type", but something else—and figuring out precisely what
that "something else" is has been the main force of the past few years
in the development of cubical type theory).

As you know, the concerns that you raise only come into play in the
rule's full generality at a non-empty context, which leads me to clarify
that the real "dangerous" force of equality reflection has little to do
with equality, and everything to do with the following position (which
you are free to accept or to reject depending on what you want to use
type theory for):

    The meaning of "G !- P true" (i.e. P under hypothesis) is completely
    defined from the meaning of "G" and the meaning of "P" under no
    hypotheses.

Indeed, the standard semantics for type theory are arranged in this way.
Nonstandard semantics, including categories-with-families, follow the
approach pioneered in universal algebra, where the meaning of a type the
specification of its closed members, but rather specifies in addition
what its members shall be under an arbitrary context, subject of course
to various coherences with substitutions.

Anyway, it's fine to want strong normalization (that is, normalization
in any context, even an inconsistent one!) & decidability—I can think of
a million places where I *do* want this. But let's be precise and
collegial with our language instead of throwing around phrases like
"really bad"—there's no point to be insulting a body of theory which has
been incredibly successful and useful, and by extension, to insult &
dismiss the people who work on it, such as myself, my advisor, and many
of my friends and heroes.

Thanks,
Jon

On Mon, Jul 18, 2016, at 01:45 PM, 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.
> 
> -- 
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.