Re: [HoTT] Different notions of equality; terminology

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

On Mon, Jul 18, 2016, at 03:20 PM, Andrew Polonsky wrote:
> That may all be true.
> 
> Yet, -- in this particular case -- it may actually be a good idea NOT
> to depart completely from the traditional, intuitive meaning of
> "logical".
> 
> The point is that here we are talking about what is really the most
> elementary, the most canonical, the most ancient concept of equality.
> The adjective "typal" suggests that something new happened when we
> transitioned from FOL to MLTT.  But that change, whatever you call it,
> (higher-dimensionality?) -- it affected equality in the same way as
> all other formulae.
> 
> So it is not a new concept.  It is the same concept.
> 
> Regarding "judgmental" equality, this is a special case of
> definitional equality.  Some formulations of type theory have it,
> others don't.
> 
> For example type theories implemented in the Coq and Agda proof
> assistants, they do not have judgmental equality.  In PTS formulations
> of type theory, definitional equality is not a judgment.

This is false, as far as I am aware. From what Peter Dybjer told me,
Agda is based on an extension of Martin-Löf's Logical Framework +
Monomorphic Theory of Sets (these are described in "Programming in
Martin-Löf's Type Theory"). Now, there's some differences between Agda's
type theory and MLLF+MTS, but both absolutely have judgmental equality.

I am not familiar enough with Coq's type theory to comment on it.

Kind regards,
Jon


> 
> Cheers,
> Andrew
> 
> On Tue, Jul 19, 2016 at 12:02 AM, Michael Shulman <shu...@sandiego.edu>
> wrote:
> > I have been advocating the term "typal equality" for what used to be
> > called "propositional".  It is less awkward than "type-level" or
> > "type-theoretic", and conveys exactly what is meant, namely that the
> > statement of equality *is a type*.  I prefer it to "logical equality"
> > because traditionally, "logic" has often referred only to the type
> > theory of mere propositions, so "logical equality" has something of
> > the same problem as  "propositional equality".
> >
> > (For the same reasons I prefer "judgmental equality" because it
> > conveys exactly what is meant in that case, namely that the statement
> > of equality *is a judgment*.  Sometimes it is accurate to call it
> > "definitional equality", but it is not always the case that such a
> > statement of equality *is a definition*.)
> >
> > On Mon, Jul 18, 2016 at 5:45 PM, Andrew Polonsky
> > <andrew....@gmail.com> 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.
> 
> -- 
> 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.