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

> 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!


On Fri, Jun 1, 2018 at 1:59 PM András Kovács <putta...@gmail.com> wrote:

> 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.
>

 If we don't intend our type theory to be used as a metatheoretical setting
for mathematics, it seems interesting to consider for example a type theory
with a family of base types indexed by the circle, the syntax of which I
think would not form a set.
That is, if we have a way to represent dependent type theory in Coq, what
happens if we add a constructor `a_circle_of_types : circle -> type` to our
syntax (for a postulated circle, or HIT)? This should be consistent, to add
a family of uninterpreted types, but I believe equality is no longer
decidable (since equality of circle is not decidable).

- Jasper Hugunin