> In essence the situation is similar to how the free oo-group on one
> generator (the integers) happens to be a set, because we can define
> "normal forms" for integers as positive or negative unary natural
> numbers.  This sort of thing is also known to happen elsewhere in
> higher category theory; for instance, the free bicategory on a
> directed graph happens to be a 1-category, because instead of
> constructing it by throwing in all binary composites, associativity
> isomorphisms, and so on, we can normalize all bracketed composites to
> be (say) left-associated.  This is essentially cut-elimination for
> unary simple type theory.
>
>
Yes, and there are of course other examples.
Like finite sets and bijections being the free symmetric monoidal category
on an object.
And Delta as the free monoidal category with a monoid.
Both of these statements are true whether I consider their higher versions
or not.
So I am aware of this phenomenon, which is why I believe the conjecture.


> So, if we have a type theory for elementary infinity-toposes that has
> normalization (perhaps some form of cubical type theory), then I would
> believe the conjecture should hold fo them too.  Note that this
> doesn't mean that the *objects* of the free elementary infinity-topos
> are *internally* sets -- that would certainly be false since it
> contains universes.  Instead, it means that the free elementary
> infinity-topos can be *presented* by a structure (e.g. a CwF) that is
> *externally* a set, just as the model category of simplicial sets is
> itself a 1-category despite containing objects that are "internally"
> (in the model-categorical sense) not sets.
>

Hmmm.  But isn't this situation different from the previous one?
Assuming there is an infinity category of elementary infinity-topoi, then I
can ask the same question as before: is the initial such guy a 1-category.
This is what, to me, the previous conjecture about categories with families
was about.
But now this time you use the word "presented", so I'm not sure if you are
making a similar statement or not.
For example, if this really were the case, wouldn't it rule out effectivity
of (even finite) colimits?
You'll have to remind me, but I think epis are still regular in an
elementary 1-topos....
So in the infinity case, wouldn't this be making kind of a big concession?

It seems to me that the question of whether syntax should be decidable
> seems to be just a question of definition as to where you draw the
> line separating syntax from semantics.  Does a HIIT initial
> infinity-categorical structure that is not decidable count as
> "syntax"?  Is it "syntax with a heavy flavor of semantics", or is it
> "semantics with a heavy flavor of syntax"?


Right, completely agreed.
I guess my position would be that, if we don't allow ourselves to think of
a HIT presentation as syntax for a higher object, if we insist that the
word syntax be reserved for set level objects, then higher objects *don't
have syntax by definition*!
That seems surprising, since the point of this list seems to be that we
have found ways to manipulate them syntactically.  :)

Moreover, there's another reason that this would be strange:
I mean, after all, kind of the whole point of introducing higher algebraic
objects is that these objects carry explicit witnesses for all of the
relations they satisfy.
And our usual way of equipping objects with this kind of witness is to
invent syntax for it.
So shouldn't it somehow be exactly the opposite: shouldn't we think of
higher objects as *more* syntactic than their set theoretic counterparts?

Whatever we call them,
> such things are certainly interesting!  But I'm dubious that we could
> use them as a foundation for mathematics unless there is also an
> untyped extrinsic syntax that can be typechecked into them (which
> might or might not require them to be decidable).
>

Yes, indeed.  Interesting and puzzling.
And I get your point here.

E.