>
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>