On page 9 of the paper Simplicial Model of Univ. Foundations, we have the following brief discussion of consistency:
It seems that, assuming soundness, in type theory we have that any theory with a model is consistent. But then it must be the case that there is never such a section of $p_{0_1}$, correct? If this is correct, then how do we verify that such a section is never possible? If not, then how do we prove that having a model implies consistency (presumably in a way similar to the classical version, which follows easily from soundness)?
This is not the case. For instance, every algebraic theory has an initial and a terminal model, but neither of these have a bearing on consistency.
The initial model is the syntax of a theory, and consistency is a statement about definability in the syntax. So the initial model is just part of the setup. The terminal model is a model where all underlying sets are given as the singleton set; e.g. the terminal category is the singleton category. Terminal models don't imply anything about the syntax; they're trivial.
There can be other models, neither terminal nor initial, which interpret the empty type as a nonempty set, and thus don't imply syntactic consistency. Consistency only follows from a model which interprets the empty type with an empty set or an analogous "empty" structure.