> > I don't think the initial model is a set. Is it?
>
> This is the big conjecture that Thorsten and I actually agree on: that
> the initial infinity-CwF in fact happens to be a 1-CwF.  Thorsten
> wants to prove this by explicitly constructing the initial
> infinity-CwF and then proving that it is a 1-CwF; my preference would
> be to construct the initial 1-CwF in a careful way (e.g. with only
> normal forms and hereditary substitution) so that one can prove that
> it is in fact the initial infinity-CwF as well.  But in both cases the
> conjectured result is the same, and even the important ingredient in
> the expected proof is roughly the same: the existence of normal forms
> and normalization.
>
>
Right, and I think I'm more or less on board with the conjecture.
Although as you start adding more structure to your CwF, things get a bit
murkier...
Is it still okay with dependent products ... umm ... and what about if I
add a class of HIT's?
To take things really far: if there is such a thing as the free elementary
infty-topos, is it a 1-category?
This somehow seems dubious, no?

So it seems to me at some point, something has to break in our notion of
what syntax for higher algebraic objects *is* in the first place.
Which is why I would not want to make the assumption from the outset that
syntax must necessarily be decidable.