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