Re: [HoTT] A small observation on cumulativity and the failure of initiality

[Andrej Bauer <andrej...@andrej.com>]

> In our recent work on intrinsic
> syntax of Type Theory we present a typed syntax that never refers to
> preterms. In this framework theories with coercions cannot be expressed
> and the syntax is the initial algebra of the corresponding notion of
> algebras.

This is quite cool, but I'd just like to point out that there are
levels of abstraction, some of which cannot be ignored.

At a very banal level, we need to know how to convert concrete syntax
into abstract syntax.

At a slightly less banal level, we have to admit that preterms
(expressed as abstract syntax) are unavoidable. An important aspect of
type theory revolves around making sure that the thing written down
makes sense. The "thing written down" is a preterm (something that
survived parsing but has yet to be type checked).

There is also the question of breaking the vicious circle: we express
type theory inside type theory, but where did the original type theory
come from? I think it is quite reasonable to take the possition that
type theory is primitive, but it is also equally reasonable to take
the position that one should analyse how type theory arises from a
more concrete setup, for instance, there is some value in knowing that
the syntactic models based on concrete syntax are initial for type
theory.

With kind regards,

Andrej