From: Martin Hotzel Escardo <escardo...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: Different notions of equality; terminology
Date: Tue, 19 Jul 2016 16:19:34 -0700 (PDT) [thread overview]
Message-ID: <ea278afa-1cb0-456e-8fe3-511db20676a0@googlegroups.com> (raw)
In-Reply-To: <b8aa1ee7-80a9-497b-916b-8b31d6eb76b3@googlegroups.com>
[-- Attachment #1.1: Type: text/plain, Size: 5357 bytes --]
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.
>
>
[-- Attachment #1.2: Type: text/html, Size: 6481 bytes --]
prev parent reply other threads:[~2016-07-19 23:19 UTC|newest]
Thread overview: 17+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-07-18 20:45 Andrew Polonsky
2016-07-18 21:03 ` [HoTT] " Andrej Bauer
2016-07-18 21:05 ` Vladimir Voevodsky
2016-07-18 21:13 ` Andrew Polonsky
[not found] ` <2506A3A8-8AC0-4B49-AD1E-D660A7A15245@ias.edu>
[not found] ` <CABcT7WDYqUY=efCTvdRpdW98aDSXpjfHGo9pJz2jBNa3yNXCgQ@mail.gmail.com>
[not found] ` <085E4ACF-BD06-484F-ACA3-17DD6249CF76@ias.edu>
[not found] ` <CABcT7WBKxFhcvuBP66wOcUzU1uPNUqPqXoSYW4aCJv4c8U7iuQ@mail.gmail.com>
2016-07-18 21:45 ` Vladimir Voevodsky
2016-07-18 21:16 ` Dimitris Tsementzis
2016-07-18 21:17 ` Jon Sterling
2016-07-18 21:24 ` Andrew Polonsky
[not found] ` <CAOvivQyZzdyhFFPfqkH4W+Z--78t0LEVWtthLhCpDxUkJNUrMQ@mail.gmail.com>
2016-07-18 22:20 ` Andrew Polonsky
2016-07-18 22:24 ` Jon Sterling
[not found] ` <CAOvivQy44FvN_bVD+nby8t0BnnTYf38dR5=s31_Yv_VsDOzLCA@mail.gmail.com>
2016-07-18 22:43 ` Andrew Polonsky
[not found] ` <CAOvivQw15pOvi9wzWFpB2WcwmgxB=uw-826xNmxUck57VagEQA@mail.gmail.com>
2016-07-18 23:01 ` Andrew Polonsky
2016-07-19 12:53 ` Michael Shulman
2016-07-19 16:49 ` Jon Sterling
2016-07-19 19:07 ` Egbert Rijke
2016-07-20 2:45 ` Dan Licata
2016-07-19 23:19 ` Martin Hotzel Escardo [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=ea278afa-1cb0-456e-8fe3-511db20676a0@googlegroups.com \
--to="escardo..."@gmail.com \
--cc="HomotopyT..."@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).