Interesting the nature of that article by Buzzard (arXiv:2405.10387).

It starts out on p. 1 with the phenomenon of non-unique isomorphism, but on p. 3 complains that the notion of equality in HoTT is “too weak, as things can be equal in more than one way”.

I can understand that a practitioner in proof formalization may find 0-truncated systems more convenient and as such not find the further expressive freedom in HoTT to be useful.

But a general treatise on the notion of equality might be more clear on the role of non-unique identity proofs.

]]>Adding reference:

- Kevin Buzzard,
*Grothendieck’s use of equality*(arXiv:2405.10387)

Anonymouse

]]>fix typo

Anonymous

]]>split contexts not needed for propositional equality

Anonymous

]]>added section about equality in classical and constructive mathematics

Anonymous

]]>added section on syntactic equality and alpha equivalence

Anonymous

]]>moved information regarding conversional equality over to conversion rule

Anonymous

]]>Similarly moved to definition

Anonymous

]]>Most of the material on definitional equality moved to definition since it was actually about defining things using equality

Anonymous

]]>Added rules for definitions

Anonymous

]]>Added a table distinguishing the different notions of equality

Anonymous

]]>Expanded lede of type theory section

Anonymous

]]>Added a section on comparing judgmental and propositional equality

Anonymous

]]>One should also distinguish between equality of terms and equality of types. Identity types are only for equality of terms, while judgmental equality comes with variants for both equality of terms and equality of types.

Similarly with computational equality, the notion of definitional equality of terms could be expressed in both judgmental and typal variants. Judgmental equality is used for definitional equality in the type theories with judgmental equality, such as Martin-Löf type theory and cubical type theory. The identity type is used in objective type theory for definitional equality of terms, as there is no judgmental equality, and everything is done through transport.

]]>One should also distinguish between typal equality (i.e. the identity type), and propositional equality (i.e. the type theory has two layers, one for types and one for propositions, and equality is a proposition).

]]>Moving the stuff about judgmental equality to its own section

Anonymous

]]>The notions of “computational equality” and “judgmental equality” aren’t the same. Judgmental equality is the equality which is defined as a judgment. Computational equality is the equality used in the beta conversion rules of types, and it could either be judgmental, as in Martin-Löf type theory for types which are not higher inductive types, or propositional, as in

- objective type theory
- the computational rules for paths in higher inductive types in Martin-Löf type theory
- the identity types of higher observational type theory
- the cubical path types of cubical type theory

Moving the stuff about objective type theory to the right section “computational equality” rather than “definitional equality”.

Anonymous

]]>adding sentence saying that objective type theory does not have definitional equality

Anonymous

]]>In my opinion, propositional equality in the context of type theory should be called “typal equality”, because many type theorists nowadays don’t call types “propositions”; they only call the (-1)-truncated types “propositions”. So “proposiitonal equalty” should be restricted in usage to the identity types which are actually valued in propositions/subsingletons/(-1)-truncated types.

]]>adding some more information about definitional equality

Anonymous

]]>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? ]]>