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

Why? The syntax being a set doesn't imply that models also need to be sets. As I understand, the goal of higher models for TT is to get rid of set-truncation but still have a syntax which is a set.

But, then, this seems to be a statement about *extrinsic* syntax. If,
as Thorsten advocates, we somehow manage to produce a highly
structured, internal description of the syntax of type theory,
then typechecking for this syntax is, by definition, unnecessary!

Type checking must be performed in any case, at some level. If we use intrinsic embedded syntaxes, then the implementation of the metalanguage (in a meta-metalanguage) does the type checking. Hence, if we intend to formalize a syntax of type theory which is intended as a metatheoretical setting for mathematics, then I think decidability is quite important.

2018-06-01 21:55 GMT+02:00 Martín Hötzel Escardó <escardo...@gmail.com>:

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

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.