is judgmental equality real?

[Michael Shulman]

A number of people seem to feel that judgmental equality is something
purely "syntactic" and doesn't express any real property of the
"things" we study in type theory. I used to think this too, and I
wish I still could, but right now it doesn't seem justifiable to me.

There is, of course, a syntactic side to judgmental equality. Namely,
we can define an equivalence relation on terms whereby M~N if the
judgment M≡N can be derived. This syntactic equivalence relation, and
its algorithmic representations, are very important, especially when
implementing type theory and/or regarding it as a programming
language. But it's not all there is to judgmental equality.

Moreover, in principle this equivalence relation doesn't serve to
distinguish judgmental equality from typal equality at all, because we
can also define a "typal equality" equivalence relation on terms
whereby M~N if there is some term E such that the judgment E:M=N can
be derived. Of course that equivalence relation is not as useful or
important. But the point is that just as there is more to the
identity type than the equivalence relation it induces on syntax,
there is more to judgmental equality than the equivalence relation
*it* induces on syntax.

What more? Well, when type theory is presented in the usual way, as
in section A.2 in the book, judgmental equality is (surprise) a
judgment. That means it is the same sort of thing as a term judgment
"M:A", and so it must be just as "real" a notion as "element of a
type".

More precisely, from a semantic perspective, type theory is (we
hope/expect) a presentation of the initial object in some category of
gizmos. The standard sort of gizmo used (which goes by various names
under various slight variations) is a category of some sort with a
fibration of types over it. In such a gizmo there is a real notion
that corresponds to judgmental equality, namely equality of morphisms
in the category (which is, of course, a different thing from sections
of the identity types).

For one thing, that means that in all the categorical models of type
theory that we know, judgmental equality (or whatever we want to call
it) exists as a semantic thing. But even if we don't have a
particular model in mind, even if we work with type theory as a formal
system and just have some *intuitive* idea of what its symbols "mean",
it seems that it would be most reasonable for our intuitive "things"
that these symbols "refer to" to be thought of as forming one of these
same gizmos, since the general way that the syntax of type theory is
made to refer to things is to make the things into a gizmo. Thus,
even in our intuitive picture of the "meaning" of type theory there
should be a notion of judgmental equality. And this is true whether
or not we reify that notion with a pretype as in HTS.

The only way I can imagine to get out of this conclusion is to somehow
present type theory so that judgmental equality is not a judgment.
One way I can imagine to do this would be to define judgmental
equality as a relation on raw untyped terms, and then quotient by that
equivalence relation before defining the other rules; so that in the
judgmental expression of type theory, wherever we see a "term" it
would actually be a judgmental-equivalence-class of terms. Another
way would be to present type theory in an LF-like way where only
canonical forms exist, and then define noncanonical terms and
judgmental equality of those as an extra layer on top, so that
"meaning" factors through the world of canonical forms where there is
no need for judgmental equality.

However, while I'm not an expert, my impression is that neither of
those approaches would work beyond a restricted class of type
theories. (If I'm wrong, please enlighten me!) But more importantly,
I don't see how to make either of them work semantically: in no
categorical model that I can think of is there a notion that could
correspond to "untyped term" or "canonical form". So it seems to me
that unless one views type theory itself as nothing more than syntax,
there is no basis for regarding judgmental equality as nothing more
than syntax.

I hope, however, that someone can prove me wrong.

Mike

[Jon Sterling]

Hi Mike,

[The tl;dr of this mail is that I think your inclination is right,
namely that judgemental equality is semantic, not syntactic—and to lend
credence to your fear that it is unavoidable (but I think this is a good
thing!).]

I can't comment on categorical models, but I will just say what I know
about a particular class of models which embody the "standard semantics"
for type theory, namely the PER models which generalize realizability
from unary logical relations to binary ones.

In the PER models of type theory, the judgmental equality is the most
fundamental notion of all, and comes before “membership”, which is
defined in terms of equality. The relation that each type denotes *is*
the judgmental equality at that type...

As a matter of policy, the "typal equality" ought to be nothing more
than an internalization as a type of a type's denotation (its PER). If
your PER model is based on closed terms, then equality reflection is
unavoidable—but if you follow Coquand or Dybjer and give a model that is
based on open terms, I think this won't be the case (can anyone
confirm?). [Clearly some iterated PER construction is required, if HoTT
is going to have an analogous treatment.]

Let me briefly comment on your two alternatives:

1. judgmental equality *is* already defined as a ternary relation on
untyped terms, since you can't even talk about typed terms until you
have defined equality. (in Martin-Löf's original meaning explanation,
I'll admit that it is the other way around, but Stuart Allen's PER
semantics are profoundly simpler, and more useful.) But I am not sure
how defining equality as a relation on untyped terms (as it is already
defined) somehow would prevent it from being a judgment, since this is
precisely how you go about defining such a judgment anyway—nor why one
would wish equality to not be a judgment.

2. Your intuition about the Canonical LF-style approach is, to my mind,
a good one; for a certain restricted class of very cleverly constructed
*closed* type theories, you don't need any equality beyond alpha
equivalence. But for type theory in general, which is an *open* system,
this won't work.

I would also comment that from a meaning-theoretical point of view, it's
important that anything that we talk about at the level of types be
reducible to some prior concept at the level of judgments /
assertions—this is what Heyting was talking about when he said that to
know that something is a proposition is to have recognized its
intention. This betrays the pervasive subjective and anti-realist
character of type theory—objective matters are *always* reduced to
subjective ones.

So what about your original comment about feeling uncomfortable with the
idea that judgmental equality is "purely syntactic"? I strongly agree
with you—because judgmental equality is not syntactic, it is semantic.
From my perspective, *the judgmental equality is literally the essence
of a type*, which is surpassed in importance by no other part of type
theory—and the only thing that causes it to seem overly syntactic is the
fact that formal type theory is not defined over closed terms, but
rather over open terms, which themselves are the source of this
distasteful "syntactic" feeling. It's for this reason that I won't be
satisfied unless HoTT can have a treatment based on closed terms—it
seems as though HTS may relate to the end goal in the same way that the
mostly imaginary "ETT" system relates to MLTT 1979 or Nuprl/CTT…

Best,
Jon

> --
> 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.

[Andrea Vezzosi]

Can the PER model be formulated as a category of some sort (i.e. one
of the standard gizmos) such that judgemental equality corresponds to
equality of morphisms?

Best,
Andrea

[Martin Escardo]

On 04/09/15 03:53, Michael Shulman wrote:
> A number of people seem to feel that judgmental equality is something
> purely "syntactic" and doesn't express any real property of the
> "things" we study in type theory. I used to think this too, and I
> wish I still could, but right now it doesn't seem justifiable to me.

Consider, in some intensional MLTT, f,g:N->N defined by

f(0)=g(0)=1, f(n+1)=(n+1)*f(n), g(n+1)=g(n)*(n+1).

We have an equality p(n) : Id f(n) g(n), by induction on n. But f(n) and
g(n) are not convertible or judgementally equal.

I think of the equality p(n) as relating the *numbers* f(n) and g(n)
(here thing=number).

But to discuss whether f(n) and g(n) are convertible, which they are
not, it is not enough to talk about numbers, as here f(n) and g(n) are
the same number. We need to talk about numerical expressions (terms) to
be able to say that f(n) and g(n) are not convertible. Conversion (in
intensional type theories) is not a relation between numbers, but
between numerical expressions.

Which conversions hold or fail determines which terms are well formed or
not, and this is very visible in Agda and Coq when you try to get them
to accept your input, and is the nature of intensional MLTT.

If conversion is made finer in a model, then this is a model of a
"larger" type theory (a type theory with more terms), which is not
necessarily bad per se, but means that the initial model (if it exists)
may not be what you call the syntax.

If conversion is regarded as a relation between things, as you and
several other people advocate, so that we have a generalized algebraic
theory, then the initial model [assuming it exists] will say that, in
the example above, f(n) and g(n) are convertible. So then is the initial
model really the syntax? It seems that this initial model will have more
terms than intensional MLTT really does have. (For example, the naive
term expressing the associativity of vector concatenation, which doesn't
type check, does type check if conversion on N is taken to mean equality
of numerical value.)

I think that either (1) conversion should not be interpreted (like you
sketch below), or (2) a subtler treatment of conversion (such as maybe
HTS) is needed to have a well behaved type theory in which the initial
model (exists and) is what we would like to call the syntax (and
probably decidability of type checking will be lost, but I am fine with
this).

Martin

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Andrej Bauer]

Echoing some thoughts by those who came before me here:

To understand how what a concept is about you have to look at how it
is used. Where us judgmental equality used? In the convertibility
rules, such as

e : A A ≡ B
--------------------
e : B

Semantically this says that judgmentally equal types denote the same
object, I think.

Where else? In the *substiution* rules, which say things like

(e₁, e₂) σ ≡ (e₁σ, e₂σ)

and

Γ, x : A ⊢ e : B Γ ⊢ e' : A
---------------------------------------
Γ ⊢ e[e'/x] : B[e'/x]

We should call it *substitutional* equality, as Vladimir says occasionally.

Now we might ask: but why does substitution need a notion of equality?
Can't we have just substitution without equality? (NB: rewrite rules
are directed equalty.) Well, we might but how are we going to do
*anything* with substitution then? How will we explain how to use
substitution?

This can be a way of explaining judgmental equality without draging in
categories then: type theory, like any other formal system, needs
methods of construction and manipulation of expressions. A basic such
method is substitution, whose laws are expressed with equations, hence
we need a notion of "substitutional" equality.

A remark: even in category theory equality of morphisms is the
"substitutional" equality, for equal morphisms may be freely
interchanged in any commutative diagram.

I like Martin's challenge: to find as *unsyntactic* model as possible
in which the morphisms denoted by

a : N, b : N ⊢ a + b : N

and

a : N, b : N ⊢ b + a : N

are not equal. How many beers is that?

With kind regards,

Andrej

[Andrej Bauer]

> To understand how what a concept is about you have to look at how it
> is used. Where us judgmental equality used?

Apologies, I should either turn on the spell checker or take an online
test for dyslexia.

[Thomas Streicher]

The judgemental equality should be decidable in the initial model but,
of course, not in the particular models arising from, say, model structures.

Thomas

[Thomas Streicher]

On Fri, Sep 04, 2015 at 08:39:03AM +0200, Andrea Vezzosi wrote:
> Can the PER model be formulated as a category of some sort (i.e. one
> of the standard gizmos) such that judgemental equality corresponds to
> equality of morphisms?

yes, since the realizability models are models of extensional type theory

Id is interpreted as fibrewise diagonal

Thomas

[Peter LeFanu Lumsdaine]

I‘m not quite sure I understand Mike’s question.  Insofar as I do, it seems to me to be another object theory/meta-theory distinction.  In the language of the object theory itself, judgemental equality is not a property of the things we are talking about — because the properties we can talk about are precisely those expressed by types, and (unless one has a reflection rule) judgemental equality is not expressed by a type.  In the language of the meta-theory — whether we’re thinking about the syntax, or a model — it certainly is a property of the “things”, either of terms or the morphisms that will model them.  But this seems like too simple a resolution, so I guess I may be missing the point of Mike’s question.

Also, as I think I’ve said here before, I believe judgemental equality is not so peculiar to type theory as it may seem.  In standard mathematical prose, one often writes e.g. “by definition, (…) = (…)”; and the way that this is used in practice seems to correspond pretty well to a notion of judgemental equality.  In particular, it’s invoked to justify steps of an argument, but it’s not itself reasoned about by general logical arguments.  Nobody writes “Lemma 5: By definition, (…) = (…).”  Instances of it usually seem to be produced by combinations of: symmetry; transitivity; congruence for all constructions, including the ξ rule (congruence for binders); δ-expansion (expansion of definitions); β-reduction; and, perhaps less often, ι-reduction (computation of recursively-defined functions).

So even if it is “just syntax”, that doesn’t mean “just a technicality of the syntax of type theory”.  It seems to be a natural part of reasoning in a formal language (even if many systems evade it by delegating the machinery of definitions and functions entirely to their meta-theory).

–p.

[Alexander Kuklev]

> One way I can imagine to do this would be to define judgmental equality as a relation on raw untyped terms, and then quotient by that equivalence relation before defining the other rules; so that in the judgmental expression of type theory, wherever we see a "term" it would actually be a judgmental-equivalence-class of terms.

That's exactly how I'd like to view syntax: an inductively constructed set of terms modulo mutually inductively constructed equivalence relation on them so that all the rules actually work on equivalence classes. And that's exactly what Thorsten Altenkirch and Ambrus Kaposi have recently achieved for a simple dependent type theory: http://www.cs.nott.ac.uk/~txa/publ/tt-in-tt.pdf

This view also makes clear that in all categorical models the morphism equality cannot be finer than the judgemental equality on terms, and in the initial model it should be equivalent to it. 

Thanks,

Alex

P.S. My great hope is that the stunt of Thorsten and Ambrus can be also performed for HoTT (with HITs and Reedy-limits) yielding a proof that HoTT (with HITs and Reedy-limits) with n universes can be modelled in HoTT (with HITs and Reedy-limits) with n+1 universes and a nice way to reason formally about HoTT using a HoTT-based proof assistant. But it's a long way to go thanks to semisimplicial types problem. HTS-like systems introduce "evil" things (such as strict equality) into the type theory and thus void the most beautiful feature of the theory, but there is some hope that with help of very-dependent types (hypothetical syntactic manifestation of Reedy-limits) it will be viable to define presheaves on inverse categories (and probably their generalizations up to something like elegant generalized-Reedy (∞,1)-categories) in bona-fide non-evil HoTT, which should be sufficient to define syntax (in the above sense that includes quotient by judgemental equality) of cubical type theory and its standard model (and perhaps also its presheaf models over arbitrary elegant generalized-Reedy (∞,1)-categories).

[Michael Shulman]

On Fri, Sep 4, 2015 at 12:15 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Conversion (in
> intensional type theories) is not a relation between numbers, but
> between numerical expressions.

I'm not sure exactly what you mean by a "number", but my best guess is
that you mean an element of the interpretation of N in some model. In
that case, my argument is that the numbers in any model do have both a
notion of judgmental equality and a notion of typal equality, which
may not be the same. In particular, they differ in the term model.

It sounds as though by "conversion" you are thinking of the
equivalence relation I described on numerical expressions that is
induced by judgmental equality. It's true that *that* is a relation
on numerical expressions, by definition; but I'm saying that in any
model (not just the term model) the "numbers" must also have a notion
of "strict" or "judgmental" equality. You may be used to thinking of
models (such as sets, or even simplicial sets) in which this equality
coincides with the typal equality, but it's not true in all models.

Mike

[Michael Shulman]

On Thu, Sep 3, 2015 at 9:20 PM, Jon Sterling <j...@jonmsterling.com> wrote:
> 1. judgmental equality *is* already defined as a ternary relation on
> untyped terms, since you can't even talk about typed terms until you
> have defined equality.

No, this is not the case in type theory as presented e.g. in A.2 of
the book. There judgmental equality at a type is "defined" as part of
the mutual induction that also "defines" term membership. One of the
defining clauses of that induction is that term membership is
coerceable along judgmental equality.

I was under the impression that judgmental equality had to be defined
in a type-directed manner in order to obtain things like judgmental
eta-rules for functions. But maybe that is a mistake?

> But I am not sure how defining equality as a relation on untyped

> terms... somehow would prevent it from being a judgment, since this

> is precisely how you go about defining such a judgment anyway

Think like a mathematician for a moment. In the usual presentation of
type theory, the metavariables denoting terms, types, and contexts in
the rules denote expressions. I'm saying that if we defined untyped
equality first and quotient by it, then those metavariables could
instead range over equivalence classes of expressions. In particular,
therefore, the "coercion rule" (if M:A and A≡B then M:B) would not be
needed, because "A≡B" would mean that the metavariables A and B
literally denote the same thing.

If you insist on it, the untyped equality could also be defined by a
judgment (reasonable, I suppose, since it is an inductive definition).
But this judgment would not be part of the same mutual induction that
defined term and type judgments, so that -- in principle, at least --
the "meaning" of type theory could factor through it and we would not
have to give a meaning to judgmental equality in models. (However, as
I said, I don't see how to actually make sense of that in any concrete
mathematical model.)

Mike

[Michael Shulman]

On Fri, Sep 4, 2015 at 6:10 AM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> In the language of the
> meta-theory — whether we’re thinking about the syntax, or a model — it
> certainly is a property of the “things”, either of terms or the morphisms
> that will model them.

This really is all I'm saying. It sounds to me as though some people
are thinking of judgmental equality as *only* a property of the
"things" in *syntax* and not a property of the "things" in models.
For instance, if I understand him correctly, Martin doesn't seem to
want "numbers" to have both a judgmental and a typal equality. I'm
just saying that it has to be there in both cases.

Mike

[Michael Shulman]

On Fri, Sep 4, 2015 at 7:13 AM, Alexander Kuklev <aku...@gmail.com> wrote:
>> One way I can imagine to do this would be to define judgmental equality as
>> a relation on raw untyped terms, and then quotient by that equivalence
>> relation before defining the other rules; so that in the judgmental
>> expression of type theory, wherever we see a "term" it would actually be a
>> judgmental-equivalence-class of terms.
>
> That's exactly how I'd like to view syntax: an inductively constructed set
> of terms modulo mutually inductively constructed equivalence relation on
> them so that all the rules actually work on equivalence classes.

That's actually the exact opposite of what I was saying. (-: What
you describe is the way I've usually seen type theory presented, and
also what Altenkirch and Kaposi do. What I'm saying is that if we
wanted to avoid having to give meaning to judgmental equality in
models, we would have to quotient by the equivalence relation *first*
before defining the other rules, so that in particular it could not be
defined mutually with them.

Mike

[Jon Sterling]

On Fri, Sep 4, 2015, at 07:59 AM, Michael Shulman wrote:
> On Thu, Sep 3, 2015 at 9:20 PM, Jon Sterling <j...@jonmsterling.com>
> wrote:
> > 1. judgmental equality *is* already defined as a ternary relation on
> > untyped terms, since you can't even talk about typed terms until you
> > have defined equality.
>
> No, this is not the case in type theory as presented e.g. in A.2 of
> the book. There judgmental equality at a type is "defined" as part of
> the mutual induction that also "defines" term membership. One of the
> defining clauses of that induction is that term membership is
> coerceable along judgmental equality.

I am distinguishing between the meaning/definition of judgmental
equality, and the particular set of rules which added to a formal system
in order to approximate it. The equality judgment is *not* defined
inductively by the set of rules that are in A.2 of the book; judgmental
equality is already fully defined in the meaning explanation (or, would
be, if there was a meaning explanation at this point), and the rules in
the appendix are just a number of useful things which happen to be
evident/valid. Which particular rules are chosen is largely arbitrary,
and they will differ from system to system, so long as they are sound
with respect to the intended semantics of type theory.

>
> I was under the impression that judgmental equality had to be defined
> in a type-directed manner in order to obtain things like judgmental
> eta-rules for functions. But maybe that is a mistake?

Judgemental equality in the sense I was talking about is defined in a
type-directed manner: namely, it is defined at each type. I was just
clarifying that the *definition* of judgmental equality is over untyped
terms, because it is the imposition of a judgmental equality which
causes a term to become typed.

>
> > But I am not sure how defining equality as a relation on untyped
> > terms... somehow would prevent it from being a judgment, since this
> > is precisely how you go about defining such a judgment anyway
>
> Think like a mathematician for a moment. In the usual presentation of
> type theory, the metavariables denoting terms, types, and contexts in
> the rules denote expressions. I'm saying that if we defined untyped
> equality first and quotient by it, then those metavariables could
> instead range over equivalence classes of expressions. In particular,
> therefore, the "coercion rule" (if M:A and A≡B then M:B) would not be
> needed, because "A≡B" would mean that the metavariables A and B
> literally denote the same thing.

Ah, indeed.

>
> If you insist on it, the untyped equality could also be defined by a
> judgment (reasonable, I suppose, since it is an inductive definition).
> But this judgment would not be part of the same mutual induction that
> defined term and type judgments, so that -- in principle, at least --
> the "meaning" of type theory could factor through it and we would not
> have to give a meaning to judgmental equality in models. (However, as
> I said, I don't see how to actually make sense of that in any concrete
> mathematical model.)

So, to be clear, I'm not arguing for an untyped equality (though, an
untyped computational equality can be very useful, as we have found in
Nuprl). I'm only pointing out the conceptual priority of equality over
membership.

Best,
Jon

[Andrej Bauer]

On Fri, Sep 4, 2015 at 5:07 PM, Jon Sterling <j...@jonmsterling.com> wrote:
> judgmental equality is already fully defined in the meaning explanation (or, would
> be, if there was a meaning explanation at this point),

Could you please elaborate on this point a bit? What is the meaning
explanation definition of judgmenal equality that would be recognized
by mathematicians as a definition in the usual sense of the word? (I
am not trolling, I really would like to know.)

With kind regards,

Andrej

[Michael Shulman]

Personally, I don't regard the "meaning explanation" as explaining
anything, nor do I believe that there can or should be an "intended
semantics". We can of course use intuitive arguments as motivation
for defining the formal systems that we do mathematics with, but the
meaning of mathematics resides in the mathematics itself.

[Alexander Kuklev]

> What I'm saying is that if we wanted to avoid having to give meaning to judgmental equality in models, we would have to quotient by the equivalence relation *first* before defining the other rules, so that in particular it could not be defined mutually with them.

Judgemental equality is an equivalence relation on terms, not on the "things" they denote, thus it is bound to leak only into the models that represent terms or their decidable equivalence classes (e.g. via morphisms) beside "things" themselves. I'd call such models syntactically faithful. 

I don't think avoiding mutuality while defining jugdemental equality would be possible for any system with decidable typechecking and definitional η-rules for functions. But mutuality does not in general guarantee "leaking" of judgemental equality into the model. For instance, one can interpret some dependent type theories with Σ-types, Π-types, inductive type families and Tarski universes enjoying parametricity into System S (a variant of polymorphic typed lambda calculus with impredicative dependent types by P. Fu and A. Stump), thus treating terms of the type theory as syntactic sugar over (αβη-equivalence classes) of raw lambda expressions (Parigot encodings of the terms), you get all α-, β- and η-rules for free definitionally and computationally. So you get a computational model quite indifferent to the notion of judgemental term equality, but at cost of the decidability of type checking.

For type systems with definitional η-rules for functions it's probably impossible to retain decidability of typechecking in a model unless it is syntactically faithful.

It does mean that judgemental equality cannot be swept under the rug as a technicality, but does not make it a less syntactical notion, for it's not a relation between representations of things in the model, but a relation between representations of terms in the model. This fact justifies the name "syntactical equivalence" for judgemental equality in non-evil theories such as HoTT. And the fact that results of computations and validity of propositions (in non-evil theories) always only depends on typal equality only, justifies dropability of "typal" in all non-metatheoretical contexts. 

Thanks,

Alex

[Michael Shulman]

On Fri, Sep 4, 2015 at 9:41 AM, Alexander Kuklev <aku...@gmail.com> wrote:
> Judgemental equality is an equivalence relation on terms, not on the
> "things" they denote

Judgmental equality "is" an equivalence relation on terms in the same
sense that belonging to some type is a property of terms. It is, but
a *corresponding* notion also has to exist in any model, independently
of the syntax.

> But mutuality does not in general guarantee "leaking"
> of judgemental equality into the model. For instance, one can interpret some
> dependent type theories with Σ-types, Π-types, inductive type families and
> Tarski universes enjoying parametricity into System S (a variant of
> polymorphic typed lambda calculus with impredicative dependent types by P.
> Fu and A. Stump), thus treating terms of the type theory as syntactic sugar
> over (αβη-equivalence classes) of raw lambda expressions (Parigot encodings
> of the terms), you get all α-, β- and η-rules for free definitionally and
> computationally.

Without knowing the details of this model, it sounds to me as though a
judgmental equality clearly *is* present in the model, namely as the
judgmental/computational equality of the System S. You didn't need to
define a *new* notion of "judgmental equality" to build the model --
you were able to use one that was already there -- but it's still
there. The fact that judgmental equality of terms can be interpreted
as judgmental equality in the model is part of what makes the model
possible.

Mike

[Andrew Polonsky]

This:

we can also define a "typal equality" equivalence relation on terms
whereby M~N if there is some term E such that the judgment E:M=N can
be derived.  Of course that equivalence relation is not as useful or
important.

 is a hilarious "Freudian" slip!

(Of course, we know what you meant.)

  But even if we don't have a
particular model in mind, even if we work with type theory as a formal
system and just have some *intuitive* idea of what its symbols "mean",
it seems that it would be most reasonable for our intuitive "things"
that these symbols "refer to" to be thought of as forming one of these
same gizmos, since the general way that the syntax of type theory is
made to refer to things is to make the things into a gizmo.

Until some time ago, my "primitive" idea of what type theory "means" was just the set-theoretic model -- dependent types are families of sets, pi-types are cartesian products, sigma-types are disjoint unions.

Simple.

Elementary.

Judgmental equality seemed like a trivial and extraneous concept in this picture.  If it was ever needed at all for the picture to make sense, that must have been in the formulation of the conversion rule.  But not in the semantics.

(In retrospect, one might admit that judgmental equality was really there all along, disguised as the set-theoretic equality of the meta-level.)

Acquaintance with homotopy type theory has forced a modification in that picture.  Now, it became impossible to take for granted that judgmental and "propositional" equality are basically the same thing. (Semantically.)

 

 So it seems to me
that unless one views type theory itself as nothing more than syntax,
there is no basis for regarding judgmental equality as nothing more
than syntax.

Mike.  Look.  All the semantic excuses you (and others) have made for judgmental equality, hinge on the validity of identity reflection.  Otherwise, the connection just isn't there, even in the most brutally minimalist settings. (Set theory.)  \n.n+1 is not judgmentally equal to \n.1+n.

Identity reflection rule is as antagonistic to pure type theory as it is to homotopy type theory.

THESIS.  Anyone who has emotional attachment to judgmental equality for semantic reasons, should admit that homotopy type theory renders that attachment obsolete.

That is the step forward.

One can also take a step backward: try to hack around different variations of identity reflection, until rediscovering that Decidability Does Matter.

Sincerely,

Andrew

[Michael Shulman]

On Fri, Sep 4, 2015 at 1:48 PM, Andrew Polonsky
<andrew....@gmail.com> wrote:
>> So it seems to me
>> that unless one views type theory itself as nothing more than syntax,
>> there is no basis for regarding judgmental equality as nothing more
>> than syntax.
>
> Mike. Look. All the semantic excuses you (and others) have made for
> judgmental equality, hinge on the validity of identity reflection.

What? Nowhere did I mention identity reflection.

[Michael Shulman]

On Fri, Sep 4, 2015 at 1:10 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> I like Martin's challenge: to find as *unsyntactic* model as possible
> in which the morphisms denoted by
>
> a : N, b : N ⊢ a + b : N
>
> and
>
> a : N, b : N ⊢ b + a : N
>
> are not equal. How many beers is that?

Here is a sketch of an attempt. In the groupoid model, N is usually a
discrete groupoid, but it doesn't have to be. Suppose we have a
sequence of trivial cofibrations of groupoids

1 --> N0 --> N1 --> N2 --> N3 --> ...

(so that in particular, each Nk is contractible) and let N =
\coprod_{k>=0} Nk. The above sequence defines 0:N and s:N->N. If P
-->> N is a fibration with given p0 : P(0) and ps : (n:N) -> P(n) ->
P(sn), we should be able to define a section by

(0a) sending 0:N to p0
(0b) extending to all of N0 by lifting isomorphisms, since N0 is contractible
(1a) define the section on the image of N0 in N1 using ps
(1b) extend to all of N1 by lifting isomorphsims, since N0 -> N1 is a
trivial cofibration
(2a) ...

Thus, this flabby N has the right eliminator to be a natural numbers
type, but there is lots of room for defining functions by recursion
with unexpected judgmental behavior.

For instance, suppose Nk is the walking iso for all k, with all the
succesor maps except the first being the identity. Then steps (1b),
(2b), etc. are vacuous and the only choice involved is that in (0b) we
get to choose where to send the "other 0", call it 0', and we can send
it anywhere that is isomorphic to p0.

[Robert Harper]

I'm a bit late to the big party, but perhaps I can usefully contribute.

To me the distinction to be made is not between "judgmental" or "propositional/typical/whatever" equality, but rather in how equality is defined.  In formal type theory all judgments, including equality, are inductively defined by a collection of rules.  The typing rules define a context-sensitive grammar for types and terms as pieces of syntax, and the equality rules define a convenient notion of equivalence of terms and types that enrich the class of well-typed terms.  Whatever the judgmental equality is defined to be, as long as it is defined by rules, it is an r.e. relation (of Sigma_1 quantifier complexity), and as such can never represent any meaningful notion of equality of mathematical objects.  In computational type theory the judgments are not defined by rules, but rather by behavioral conditions on the execution of programs that define, in particular, when two programs are equal _as elements of a type_.  The quantifier complexity of equality varies with the type, and has no a priori bound.  It can never coincide with a formally defined equality except in the most trivial cases, and certainly not for functions.  In computational type theory the rules are secondary to the semantics of the judgments, and are never to be thought of as defining those judgments.  The role of the semantics is precisely to establish a class of mathematical entities with which to work.  In particular, following the dictum "no entity without identity" (I think due to either Quine or Putnam), defining equality is of the essence of the enterprise.

It is for this reason that I insist that "ETT" defined as ITT+UIP+ER is an entirely inappropriate characterization of computational type theory.  Adding two more rules still leaves you with a formal type theory, albeit one with two more rules than ITT.  I think it is fruitless to keep bringing up UIP and ER in these discussions, because it can never get at the underlying issue, which is how the judgments are defined and not the fact that they are or are not judgments.

I will mention by way of justifying my remarks about formal type theory that there is no fundamental need in formal type theory to have an equivalence judgment at all.  As an example, one formulation of the LF type theory has no equivalence apart from alpha equivalence.  All terms are kept in canonical form, so that two terms are formally equal exactly when they are alpha equivalent.  Substitution is defined in the manner proposed by Watkins to ensure that when substituting a canonical form into another canonical form, the results is again in canonical form; this is not true for ordinary substitution, one instead uses a type-directed notion of substitution that Watkins dubbed "hereditary substitution".  This is one example of a case where a formal type theory does not even have an equality judgment; one can go further with the same sorts of ideas, even before getting to things like identification types or equality types.  For example, Arbob Ahmad, working with Dan and me, has developed such an account of the finite typed lambda calculus (unit, void, product, sum, function types) in this style.  My point here is just to mention that such formal type theories exist and are useful.

When an equality judgment is formally defined by rules as in ITT and related type theories, I think it is quite incorrect to refer to it as "exact equality" or even "equality" in the ordinary mathematical sense.  I also think that it has little to do with computation.  It is true that for certain fixed formal systems one can induce a reduction or normalization process that characterizes the formally defined equality, but that is a very brittle concept of a computational interpretation --- it does not scale to extensions of the theory.  It is, however, necessary to have a decision procedure, which is often given in this form but need not be, because of the "philosophy" of formal type theory.  Finding such decision procedures can be very difficult, depending on the rules of formal equality, and in any case requires significant meta-mathematics.  For this reason such formal theories can never, in my mind, be seen as foundational.  Rather than being a foundation for mathematics, they are inevitably a piece of mathematics (specifically, metamathematics).

Well, this should be enough to get my head bitten off and spat out again.  I hope it is of some use to further the discussion.

Bob

[Matt Oliveri]

On Saturday, September 5, 2015 at 3:24:38 PM UTC-4, Robert Harper wrote:

I'm a bit late to the big party, but perhaps I can usefully contribute.

To me the distinction to be made is not between "judgmental" or "propositional/typical/whatever" equality, but rather in how equality is defined.  In formal type theory all judgments, including equality, are inductively defined by a collection of rules.  The typing rules define a context-sensitive grammar for types and terms as pieces of syntax, and the equality rules define a convenient notion of equivalence of terms and types that enrich the class of well-typed terms.  Whatever the judgmental equality is defined to be, as long as it is defined by rules, it is an r.e. relation (of Sigma_1 quantifier complexity), and as such can never represent any meaningful notion of equality of mathematical objects.  In computational type theory the judgments are not defined by rules, but rather by behavioral conditions on the execution of programs that define, in particular, when two programs are equal _as elements of a type_.  The quantifier complexity of equality varies with the type, and has no a priori bound.  It can never coincide with a formally defined equality except in the most trivial cases, and certainly not for functions.  In computational type theory the rules are secondary to the semantics of the judgments, and are never to be thought of as defining those judgments.  The role of the semantics is precisely to establish a class of mathematical entities with which to work.  In particular, following the dictum "no entity without identity" (I think due to either Quine or Putnam), defining equality is of the essence of the enterprise.

Of course you're right that any formal system is RE and incomplete, but that seems to be missing the point of the thread. The use of an RE formal system for doing math does not need special justification, because that's something we all know about. But ITT's judgmental equality is not just RE, it's decidable. More importantly, it ends up feeling much more incomplete than the rest of the formal system, in order to be analytic. This is a more painful kind of incompleteness than Gödel's, so it begs for additional justification. Maybe computationally solving some equations is justification enough, but it's proof-theoretic justification. I think the essence of one of the questions in this thread is whether there's any semantic justification for the way judgmental equality is in ITT. In contrast, (provable instances of) typal equality, and any equality in an extensional (formal) type theory, do not need additional justification: they are incomplete only because of Gödel's incompleteness.

It is for this reason that I insist that "ETT" defined as ITT+UIP+ER is an entirely inappropriate characterization of computational type theory.  Adding two more rules still leaves you with a formal type theory, albeit one with two more rules than ITT.  I think it is fruitless to keep bringing up UIP and ER in these discussions, because it can never get at the underlying issue, which is how the judgments are defined and not the fact that they are or are not judgments.

I didn't think anyone suggested that ETT is a characterization of computational type theory. But my impression is that unlike ITT, it's rules are considered to be pretty well motivated by preexisting semantic notions.

I will mention by way of justifying my remarks about formal type theory that there is no fundamental need in formal type theory to have an equivalence judgment at all.  As an example, one formulation of the LF type theory has no equivalence apart from alpha equivalence.  All terms are kept in canonical form, so that two terms are formally equal exactly when they are alpha equivalent.  Substitution is defined in the manner proposed by Watkins to ensure that when substituting a canonical form into another canonical form, the results is again in canonical form; this is not true for ordinary substitution, one instead uses a type-directed notion of substitution that Watkins dubbed "hereditary substitution".  This is one example of a case where a formal type theory does not even have an equality judgment; one can go further with the same sorts of ideas, even before getting to things like identification types or equality types.  For example, Arbob Ahmad, working with Dan and me, has developed such an account of the finite typed lambda calculus (unit, void, product, sum, function types) in this style.  My point here is just to mention that such formal type theories exist and are useful.

(This is a cool trick. I've wondered if an all-normal-form calculus and type-directed substitution would help HoTT to eat itself. It doesn't seem to.)

And for ETT, you can eliminate judgmental equality by just using typal equality everywhere instead, and dropping ER. I think.

But there is a difference between the equalities of ITT and ETT, even when they're both given by formal rules. And I think that difference is closer to the issue than the difference between an axiomatized equality and its informal meaning.

When an equality judgment is formally defined by rules as in ITT and related type theories, I think it is quite incorrect to refer to it as "exact equality" or even "equality" in the ordinary mathematical sense.  I also think that it has little to do with computation.  It is true that for certain fixed formal systems one can induce a reduction or normalization process that characterizes the formally defined equality, but that is a very brittle concept of a computational interpretation --- it does not scale to extensions of the theory.  It is, however, necessary to have a decision procedure, which is often given in this form but need not be, because of the "philosophy" of formal type theory.  Finding such decision procedures can be very difficult, depending on the rules of formal equality, and in any case requires significant meta-mathematics.

Aside from the first sentence, I agree with this. A computational implementation of a system does not automatically make that system about computation. (On the other hand, trying to implement a system can still give clues about how to come up with a corresponding computational system.)

[Michael Shulman]

On Fri, Sep 4, 2015 at 12:15 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> Conversion (in
> intensional type theories) is not a relation between numbers, but
> between numerical expressions.

Let me ask this same question about a different example, since numbers
have too much historical baggage. Consider the two constructors of
the HIT interval (or, equivalently, ||Bool||). They are equal, but
not judgmentally/strictly/convertibly so. Is the latter failure only
a *syntactic* statement, a statement about a relation between
*expressions* whose type is the interval? Or does it reflect some
more intrinsic property of those two points? It seems to me that the
difference between the interval and the unit type is more than just
syntactic. Indeed, it has real mathematical consequences, since the
interval type implies function extensionality.

Mike

[Andrej Bauer]

Perhaps we're just looking at judgmental equality from the wrong point
of view. This reminds me of non-standard models of Peano arithmetic:
they exist only because one tries to axiomatize natural numbers in a
bizarre way (without reference to the rest of the matehmatical
universe) – as soon as we axiomatize the natural numbers as an
object/set/type with a certain initial property they are fixed (up to
equivalence of course).

Perhaps we should just do the same with judgmental equality and
incorporate it into type theory as a "first-class" citizen. I think
we'll invent HTS.

With kind regards,

Andrej

[Matt Oliveri]

On Sunday, September 6, 2015 at 4:52:25 PM UTC-4, Michael Shulman wrote:

Consider the two constructors of
the HIT interval (or, equivalently, ||Bool||).  They are equal, but
not judgmentally/strictly/convertibly so.  Is the latter failure only
a *syntactic* statement, a statement about a relation between
*expressions* whose type is the interval?

Yes, I believe so. One cannot show that the interval has more than one point, right? It seems like interval and unit could be the same type (not just equivalent), just that only one of the axiomatizations reveals function extensionality. ITT doesn't know whether they're the same type or not, which lets us suppose the interval is something else. But maybe it isn't.

(I am not proposing that we should interpret the interval and unit to be strictly the same. Just that HoTT currently doesn't seem to care whether they're the same.)

Or does it reflect some
more intrinsic property of those two points?  It seems to me that the
difference between the interval and the unit type is more than just
syntactic.  Indeed, it has real mathematical consequences, since the
interval type implies function extensionality.

That is a formal consequence of how the interval is axiomatized. It doesn't tell you whether there's anything new about the type in a given model.

[Michael Shulman]

If the unit type has a judgmental eta-rule, so that all its elements
are judgmentally equal, then it cannot be the same type as the
interval, for if zero ≡ one judgmentally in the interval then we have
equality reflection.

[Matt Oliveri]

Oh, right.

[Jules Jacobs]

We have zero = one, but:

x : F zero

f : F one -> A

f x ??

Now  F zero could be Nat and F one could be List Bool, and then f x does not make sense (or maybe it does in HTS, but equivalences between Nat and List Bool are not unique, so automatically transporting along them makes your program dependent on the whims of the type checker). So zero is not "evidently equal" to one. On the other hand, with g 0 = 1 and g (n+1) = (n+1) * g n and h 0 = 1 and h (n+1) = h n * (n+1):

x : F g

f : F h -> A

f x

is fine, semantically (of course one could interpret the syntax of type theory in a weird model that makes g and h not equal, but let's assume that we don't do that). So g is "evidently equal" to h. While ordinary judgemental equality is fairly arbitrary because it is decidable, if we want things to make sense we cannot just use propositional equality instead. Ultimately the evident equality on values is based on which types are evidently equal, and then two values x:A and y:A are evidently equal if for all F : A -> Type, F x is evidently equal to F y. In this case we can use a value of type F x in a context of type F y.

We can choose which types we make evidently equal, for example we could say that the pair type A * () where () is the unit type, is evidently equal to A by specifying a canonical isomorphism. We need to be careful that all canonical isomorphisms are coherent. For example specifying some canonical isomorphism f between Nat and List Bool is possible but if you have isomorphisms g Nat <-> A and h : A <-> List Bool then it would be nice if f = g . h, otherwise you get into situations where the a program can be ambiguous, or the meaning of your program depends on the whims of the type checker. Lastly, if we make make more things evidently equal then we can only interpret terms in the theory in models that also satisfy those equalities.

Judgemental equality is then a decidable approximation to evident equality.

P.S. Let me know if I should stop posting to this list and keep to hott-cafe; I do not wish to intrude.

[Michael Shulman]

I'm very sympathetic to the point of view that judgmental equality is
a "chosen coherent system of equalities", although as far as I know it
isn't yet really formally justified. I mean, the because the
judgmental equalities are strict, they are coherent in a certain
sense, but we don't have a sufficiently general coherence theorem
showing that any coherent system is enough to give a model of type
theory. However, if it were true, that would be a nice way to think
about the fact that every model comes with a semantic "judgmental
equality": when describing a model, we have to specify the equalities
but also a coherent subsystem of them to be the "substititional" ones,
as Vladimir calls it.

But, I don't really see why a coherent system of equalities deserves
the adjective "evident".