On Friday, 1 June 2018 18:45:42 UTC+1, Eric Finster wrote:

I guess my question is pretty simple: why should we insist,
as Thorsten seems to, that the "intrinsic" syntax of type
theory form a set?

I like this question. If the syntax is supposed to be the initial model, then it can't be a set.

Martin