From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 19 Jul 2016 16:19:34 -0700 (PDT) From: Martin Hotzel Escardo To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: Different notions of equality; terminology MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1088_627716864.1468970374183" ------=_Part_1088_627716864.1468970374183 Content-Type: multipart/alternative; boundary="----=_Part_1089_2119516281.1468970374183" ------=_Part_1089_2119516281.1468970374183 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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. > > ------=_Part_1089_2119516281.1468970374183 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Just a small remark.

It is indeed sui generis that equality in its various manifestations ha= s=20 this special status in type theory.

It is not *just* that we have different notions of equality. The notion= s=20 of equality play a fundamental role in the very <= span class=3D"moz-txt-tag">*architecture= * of type=20 theories.

The fundamental reason we need judgemental equality is, in particul= ar, to=20 make sense of type dependency.

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

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

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

Best,
Martin

On Monday, July 18, 2016 at 9:45:57 PM UTC+1, Andrew Polonsky wrote= :
Good ev= ening.

One feature of type theory which is often c= onfusing to newcomers is the presence of several notions of equality. =C2= =A0Today, at the opening of the FOMUS workshop, Vladimir gave a talk about = the very subject -- but more on that later. =C2=A0The two most common notio= ns are usually called "definitional equality" and "propositi= onal equality".

It is agreed by most members = of this list that the name of the latter notion is unfortunate, if not misl= eading. =C2=A0I would like to suggest the name "logical equality"= to be used for this notion.

First, let us summari= ze the two notions in greater detail.


1. DEFINITIONAL EQUALITY.

PROPERTIES.

- Purely syntactic: "proofs" of this equality con= cern only the way the objects are presented;
- Is always interpre= ted strictly;
- Preserved under all contexts:
=C2=A0 If= M=3DN definitionally, then C[M]=3DC[N], still definitionally;
- = Validates strict conversion rule:
=C2=A0 If t has type A, and A i= s definitionally equal to B,
=C2=A0 Then t *itself* has type B. (= Not a transport of t, nor some term equal to t.)
- Cannot be asse= rted in a derivation context [*]
- In total languages, is usually= , but not always, decidable.

EXAMPLES.
<= br>
- 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 throu= gh well-typed terms);
- Equalities which result from newly introd= uced rewrite rules;
- Equalities which result from unification/pa= ttern-matching constraints;
- Any equalities arising from quotien= ting 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;
- Ind= uces isomorphism/equivalence of fibers between dependent types; thus
<= div>- 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 ident= ity type;
- Univalent equality in HoTT/UF;
- Leibniz eq= uality 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. =C2= =A0Whether one considers equality as a "logical symbol", it is ob= viously a concept which is present at the level of *formulas*. =C2=A0Under = formulae-as-types interpretation, one would naturally tend to think of it a= s a proposition, until one came to realize that some types are not proposit= ions. =C2=A0(Indeed, it was the only dependent type former in Howard's = original paper. =C2=A0Yet it could not be iterated/applied to itself.)

The point is that the second kind of equality is the o= ne which can be reasoned about internally, *in the object logic*. =C2=A0Hen= ce, it exists not on the level of terms and definitions, but on the level o= f logic and proofs/constructions of formulae/types.


One argument against the adjective "logical" is = that it can lead to confusion with "logical equivalence". =C2=A0B= ut 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 betwe= en "substitutive" and "transportational" equalities. = =C2=A0But in his system, both concepts are of the "logical" kind.= =C2=A0The effect is therefore to promote "strict" equality to th= e logical level; so one can reason about it in the object logic, while reta= ining other properties like the conversion rule.

T= he 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 properti= es 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
<= div>
[*] =C2=A0In certain settings, one can make sense of def= initional equalities "in-context" via the so-called Girard--Schro= der-Heister (GSH) elimination rule.

= ------=_Part_1089_2119516281.1468970374183-- ------=_Part_1088_627716864.1468970374183--