search

HoTT / book

A textbook on informal homotopy type theory
2.04k stars 360 forks source link

"term" vs "element" #1120

Open ghost opened 2 years ago

ghost commented 2 years ago

On the Unimath agda library discord, Martin Escardo wrote:

When we discuss syntax, we do define the terms of a type inductively together with the types themselves, and together with more, including definitional equality. But when we are doing mathematics, types are semantical objects, just as sets are semantical objects in set theory, and so are elements of types. There is a huge difference between a term of a type (a syntactical object) and an element of a type (a semantical object).

So, I think that it would be a good idea to go through the HoTT book and replace "term" with "element" where appropriate.

mikeshulman commented 2 years ago

I don't know that Martin's perspective is universally accepted in the community. But I also don't think "term" is used much of anywhere in the HoTT Book that it could be replaced by "element". Do you have any examples in mind?

awodey commented 2 years ago

I actually disagree and prefer to use the word “term” also for semantics, but I think I lost that argument and agreed to “point” as a compromise. “Element” is simply wrong, in my opinion.