Just to say that if you are on top of these issues and have the vision and the energy that you seem to have in comment #41, then it would be best if you go ahead and make edits!

]]>I'm not an expert of all the diversity of literature on the subject but I was thinking that, maybe, it could be worth at least to make a short update of the pages judgmental equality and of the section type theory of the page equality so as to give a bit more context on the different definitions.

Typically, my basic idea would be:

- To join the paragraphs "definitional" and "computational" into one called "judgmental equality" (though still mentioning the alternative terminology "definitional" and "computational", with explanations of what they convey), with link to the page judgmental equality.

- To then restructurate the three paragraphs "definitional", "computational" and "propositional" into two paragraphs of roughly equal size contrasting "judgmental equality" with "propositional equality".

- The first paragraph would link to judgmental equality and condense the current two paragraphs "definitional" and "computational", moving part of the contents to the page judgmental equality so that the two paragraphs "judgmental equality" and "propositional equality" are well-balanced. It would discuss the different usages of the expression definitional equality (alpha-conversion, delta-conversion, optionally beta-reduction, optionally eta-conversion, ...). It would discuss the question of the decidability of the equality and of the orientation of the generators of the equality so that decidability can be achieved. I would mention the decidability issues with eta in recursive types (natural numbers, streams, ...).

I'm not familiar with the terminology computational equality and I did not find many resources about it on the web, but I will mention that it is sometimes used as a synonym of judgmental equality. I would mention the difference between typed and untyped judgmental equality telling that the terminology "convertible" is commonly used in place of judgmental equality when it is untyped, especially in the context of Pure Type Systems.

I would mention what kind of extensionality is achieved with eta-rules and that judgmental equality, thanks to the xi rule, has full functional extensionality. Maybe the xi rule should be discussed as its inclusion is sometimes questioned (see e.g. Martin-Löf 1975 http://archive-pml.github.io/martin-lof/pdfs/About-Models-for-Intuitionistic-Type-Theories-and-the-notion-of-Definitional-Equality-1975.pdf), but I know no reasonable type theory which excludes it, so maybe it is not worth mentioning the issue.

I would mention further extensions of the idea of judgmental equality, where any arbitrary complex decidable rewriting system can serve as hard-wired equality. I'm thinking here to ideas present in the Calculus of Algebraic Constructions, Coq Modulo Theories, Deduction Modulo, ... even if they break with the purely "intensional" spirit providing only the canonical beta-delta-way to compute normal forms.

- The second paragraph would list the identity type (linking to identity types), the (impredicative) definition of Leibniz equality, and the (heterogeneous) cubical equality (linking to cubical type theory even if cubical equality is not described there). It would explain that "propositional equality" is equality seen as a connective (or type former) so that it can be a component of arbitrary complex formulas. It would say that "propositional" is a historical terminology which is not necessarily well-chosen in retrospect of HoTT (since equality as a connective is not necessarily a proposition in the HoTT sense). It would explain how "propositional equality" leads to Martin-Löf's Extensional Type Theory when reflected back to judgmental equality (inheriting functional extensionality and proof-irrelevance).

Maybe should it be mentioned that several equality type formers can coexist (as in two-level type theory).

Probably further details would show up when trying to implement this plan but my first question is to get feedback on the idea. Would such update be ok for the maintainers of this page? If yes, are there things to take into account that I would not be aware of, etc.

Note: I have no idea about what ∞-reduction and ∞-conversion are. Should this be dropped? ]]>

Actually, I got error 524, so I'm not sure if it worked.

]]>I saw that propositional equality redirects to both equality and identity type, so I made it redirect only to the latter. We could similarly make definitional equality redirect to judgmental equality, except that there is very little written there, so I'm not doing that now.

]]>The page equality has some philosophical remarks. I don’t know of any formal system that has a formal notion called “definitional equality” that’s distinct from judgmental equality, but some people use them with different philosophical meanings.

]]>Should we organise things better here? We have ’definitional equality’ as a redirect for equality, and a section dealing with that form of equality on this page. Then we have judgmental equality which is all too brief. At the very least surely we need to note that definitional and judgmental equality are taken as synonyms in HoTT. Do other systems distinguish them?

]]>I don’t think I have much to add to Toby’s answer.

]]>I've written something. Mike might want to comment as well (also Tom Leinster).

]]>Would somebody be willing to answer this MO question about equality in structural set theory?

]]>Added to the References-section at *equality* a pointer to *Science of Logic*, volume 1, book 2, “Die Lehre vom Wesen”.

In some way, that makes it worse that they are nevertheless logically independent. (-:

]]>But they are all related! Each one makes sense (to me) in its own terms.

]]>Thanks. The many uses of “extensional” really are a mess.

]]>Thierry Coquand sent me further stuff by email, which has gone into the article under References (and a clarifying comment).

]]>Thanks!!

]]>I like it!

]]>I thought that what you wrote was confusing, so I did some expansion.

]]>I’ve edited equality in light of that.

]]>Yeah, we had a discussion about that somewhere around here. In fact, just above!

]]>I have no time to take care of it right now, but maybe somebody reading this here has: by email I receive the following comment on the entry *equality*:

At

http://ncatlab.org/nlab/show/equality

one can read “2+2” and “4” are not definitionally equal (but that “2” and “S(S(0))” are). Is it clear? One defines

2 = S(S(0)) 4 = S(S(S(S(0))))

and

x+0 = x x+S(y) = S(x+y)

the equality there being definitional (definition of +). It follows that

2 + 2 = S(S(0)) + S(S(0)) = S(S(S(0)) + S(0)) = S(S(S(S(0)) + 0)) = S(S(S(S(0)))) = 4

where all equalities are definitional.

Martin-Lof (in talks) had a reference to Godel’s 58 Dialectica paper (I have only the 72 version here) where he talks in footnote 7 about the equality being understood as “intensional equality… This is always decidable for two given functions”. This reference might be relevant.

]]>I don’t think I would recommend the blanket use of any particular adjective independent of the formal context, since the meaning of “presented”, “trivially”, “encode”, and “information” may vary. In a sense, higher category theory is all about distinguishing between precise gradations of the possible meanings of these words! (Also, as Toby points out, mathematicians have a distressing tendency to take words that used to be used informally and give them formal meanings, so that we have to find new words to use when we want to talk informally.)

]]>I would probably have said ‘intensional’, but maybe that’s not right if intensional equality is a formal concept in one’s language and one uses a rule stating by fiat that certain things are intensionally equal even when they do not trivially encode the same information.

]]>Hmmm... I see my confusion is not entirely endogenous, now, for I came here from HoTT-dot-o-r-g (the conversation was diverging from HoTT-proper) and the nlab page intending to quibble that " 2 + 2 = 4 " isn't part of the definition of "4" (nor of "2") but IS sometimes part of the definiton of "+"; and now I see Mike once said

many type theorists use the phrase "definitional equality" to mean "computational/conversional equality"

So... I'm not sure quite what to conclude. The practical question for me at the moment is: what adjective should one use instead of "definitional" in a publicly-readable website when one is trying to say that two structures, presented differently, still trivially encode the same information?

]]>