What are statements of HoTT that are not provable therein and thus may or may not be true in specific models, specifically models in $(\infty,1)$- topoi? I've also seen the term "classicalities" being used for such statements.
The examples I've found are:
LEM, AC, Whitehead Principle, n-types covering.
I had also noted the statement that " A set-indexed wedge of circles is always a 1-type" but I seem to have lost that reference.
Are there any other such statements?