"term" vs "element"

[ghost]

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]

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]

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.