The first-order metatheory of HoTT Does there exist a (say, simply typed) first-order theory which axiomatizes a universe of $\infty$-groupoids, in a similar manner to how ZFC can be considered as an axiomatization of the universe of sets (or perhaps as an axiomatization of what a universe of sets should look like)? The connection with the title of this question is that it seems to like this should be roughly equivalent to having a first-order metatheory of something like HoTT whose objects are to be interpeted as the types and terms of HoTT, with the native equality symbol "$=$" of the metatheory read as the judgemental equality "$\equiv$" of the type theory. (Note that it is irrelevant here that the dependent types of HoTT mimic the logical symbols $\exists,\forall$, just as the need for the logical symbols $\wedge,\vee$ in ZFC is not obviated by the fact that the set-theoretic operations $\cap,\cup$ behave similarly.)
It seems to me that HoTT does not really describe the model in simplicial sets in an entirely analogous way to how ZFC describes the set-theoretic universe. Rather (and please correct me insofar as I am mistaken!), it provides a language for doing constructions with simplicial sets (or the analogous objects in other $(\infty,1)$-toposes or something). (For comparison, ZFC allows us to formalize computations regarding concrete sets, but it also allows us to quantify over sets and therefore to reason about many distinct concrete computations simultaneously, all internally to the theory.) To illustrate the difference here, consider the deduction rule
$$
\frac{``\Gamma\vdash A:\mathcal{U}", \quad ``\Gamma,x:A\vdash B:\mathcal{U}",\quad ``\Gamma,x:A\vdash b\equiv b':B"}{``\Gamma\vdash \lambda x.b \equiv \lambda x.b' : \prod_{x:A} B"}
$$
of HoTT, which is $\Pi$-Intro-Eq in Appendix A of the HoTT book, except I've added quotation marks to emphasize that we are working with strings "internal" to the HoTT formal system. In other words, if we have already asserted strings of the form on the top line, then the programming language allows us to assert the string on the bottom line. Thus, the metatheory should have an axiom of theorem which looks something (very, very roughly) like
$$
``(\forall A,B(x:A))(\forall b,b':B)( b= b' \Rightarrow \lambda x.b = \lambda x.b')"
$$
which states in the formal language of the metatheory what the deduction rule does. (And this looks like it should follow for the axioms of equality in FOL.) Moreover, the metatheory should have some sort of axiom expressing the fact that the only types that are judgementally equal are those that can be shown to be judgementally equal via the deduction rules in Appendix A of HOTT. That is to say, ZFC has many axioms telling us that things are not equal --- e.g. the axiom defining the empty set in ZFC implies that $\varnothing \neq \{\varnothing\}$. But it seems to me (and once again, please correct me if I am mistaken) that the statement ${\mathbf{1}}\not\equiv{\mathbf{0}}$ regarding the empty and unit types is a statement in the metatheory, about HoTT, rather than a statement in HoTT itself. But $``\neg({\mathbf{1}}={\mathbf{0}})"$ should be a theorem (maybe a nontrivial one) of the metatheory.
 A: I don't really understand how the question in your first sentence is related to the rest of what you wrote.  I have a guess, but let me pontificate a bit first about how I think the comparison between ZFC and dependent type theory is usually understood.  If my answer isn't what you had in mind, maybe you can clarify what led you to ask about first-order theories of $\infty$-groupoids.
(FWIW, in my opinion, unqualified "HoTT", i.e. "homotopy type theory", refers to the entire subject area, not to a specific formal theory.  The specific formal theory of the book is sometimes called "Book HoTT".)
Deductive systems
The basic object in foundations of mathematics is a deductive system: a collection of rules for deriving judgments.  Note that a deductive system does not include any way to "reject" a judgment: all we can do with a judgment is derive or deduce it.
Dependent type theory is itself a deductive system.  Its judgments are of the form $\Gamma\vdash a:A$ and $\Gamma \vdash a\equiv b:A$, where $\Gamma$ is a context of variables assigned to types, and its rules are the sort presented in the appendix of the HoTT Book.  Sometimes one takes "$\Gamma \vdash A$ is a type" and "$\Gamma\vdash A\equiv B$ as types" as basic judgments too, although in a Russell universe system those could be identified with $A:\mathscr{U}$ and $A\equiv B :\mathscr{U}$ for some universe $\mathscr{U}$.
In the case of ZFC, things are potentially more confusing because there are two levels, the logic and the "theory".  The deductive system here is single-sorted first-order logic.  Its judgments (in a natural-deduction presentation) are of the form $\Delta \mid \Gamma \vdash \phi$, where $\Delta$ is a list of variables, and $\phi$ is a logical formula and $\Gamma$ is a list of formulas containing only the free variables in $\Delta$.  Its rules are things like the introduction and elimination rules for each connective and quantifier.  Inside this deductive system, with basic relation symbol $\in$, we then assert the axioms of ZFC.
So, at a formal level, there is no need for a first-order metatheory of type theory the same way ZFC sits inside first-order logic: type theory is its own deductive system.
Semantics
A "model" or "interpretation" of a deductive system consists, informally, of an assignation of "things" to its judgments in such a way that its rules are valid.
The usual way to describe a model of dependent type theory is to specify a category of some kind and say that the judgments are to be interpreted using objects and morphisms in that category.  (To be precise, it should be some kind of categorical model of dependent types.)  For instance, Book HoTT has a model in the category of simplicial sets in this sense.
A correspondingly general semantics of first-order logic involves a hyperdoctrine.  Very often this is the hyperdoctrine of subobjects in some category, and classically one generally restricts only to case when that category is $\rm Set$.  In the single-sorted case, we specify a single object of that category to be the type of "things", with morphisms or relations on that object corresponding to the symbols, and such that the axioms hold.  Working in $\rm Set$, we thus get the standard notion of "model of ZFC": a set $V$ together with a relation $[\in] \subseteq V\times V$ such that the axioms of ZFC hold.
There is indeed a difference here: a category such as simplicial sets in which we model Book HoTT doesn't have to "sit inside" anything else; while at least with categorical semantics phrased in this way, a model of ZFC does have to sit inside some ambient category.  However, the "quantifications over sets" of ZFC are still semantically the same sort of thing as the quantifications ($\Pi$-types) of type theory: operations on (sub)objects in some category.  A $\Pi$-type over a universe $\mathscr{U}$ in type theory seems to me like "reasoning about many distinct concrete things" simultaneously in the same way that a quantifier $\forall$ over sets in ZFC.
Note also that just as a deductive system doesn't have any way to "reject" a judgment, a model of that system doesn't have to respect non-derivability.  A certain definitional equality may not be derivable in type theory, but the analogous equality might still hold in some model.  Similarly, a certain formula may not be provable in ZFC, but it might still hold in some model.
Disequality
Disequality is confusing because first-order logic doesn't have an equality judgment.  The disequality $\varnothing \neq \{\varnothing\}$ is a formula such that the judgment $\vdash \varnothing \neq \{\varnothing\}$ can be derived.  Accordingly, in any model, the interpretation of this statement must be "true".  Note, though, that in the generality of categorical semantics, this doesn't mean that the semantical objects interpreting $\varnothing$ and $\{\varnothing\}$ are distinct: in the trivial model in the terminal category, all formulas are true, including both $\varnothing \neq \{\varnothing\}$ and $\varnothing = \{\varnothing\}$.
Analogously, dependent type theory contains a type $\neg {\rm Id}_{\mathscr{U}}(\mathbf{0},\mathbf{1})$, and a term $t$ such that the judgment $\vdash t : \neg {\rm Id}_{\mathscr{U}}(\mathbf{0},\mathbf{1})$ is derivable.
Type theory also contains a judgment $\mathbf{0} \equiv \mathbf{1} : \mathscr{U}$, which is not derivable.  This is a truly meta-theoretic statement about the deductive system, not anything inside the theory.  Importantly, therefore, it may not be respected by models; this particular example is confusing because of the positive derivability of $\vdash t : \neg {\rm Id}_{\mathscr{U}}(\mathbf{0},\mathbf{1})$.  But there are other pairs of types, like $\mathbb{N}$ and $\mathbb{Z}$, for which $\mathbb{N}\equiv\mathbb{Z} : \mathscr{U}$ is not derivable, but such that there are nontrivial models in which the interpretations of $\mathbb{N}$ and $\mathbb{Z}$ are equal (for the strict sort of semantic equality that corresponds to syntactic judgmental equality).
The analogue of this in ZFC would be a statement that a certain formula $\phi$ is not provable.  Again, this is a metatheoretic statement that may not be respected in models.  Of course, if $\neg \phi$ is provable, then $\phi$ can't hold in a nontrivial model.  But if $\phi$ is an undecidable statement like the continuum hypothesis, then it is unprovable and neverthless there are nontrivial models in which it holds.
In particular, we never assert an axiom that "the only types that are judgementally equal are those that can be shown to be judgementally equal via the deduction rules".  Syntactically, this statement is just true by definition: what it means for two syntactic types to be judgmentally equal is that they can be shown to be so by the deduction rules.  And semantically, this statement is generally false: any given model will validate (the interpretations of) more judgmental equalities than are derivable syntactically.  Analogously, in first-order logic we never assert that "the only formulas that are provable are those that can be shown to be provable via the rules of logic" --- this is either a definition of "provable" or a false statement for any particular model.
Conclusion
I hope I've explained clearly how the differences between ZFC/FOL and dependent type theory manifest from viewing them both as deductive systems.  The differences come from differences in the presentations, such as the presence or absence of an equality judgment, the presence or absence of multiple types/sorts, and so on.
Given that, I don't entirely understand how a "first-order metatheory of Book HoTT" would be related to a first-order axiomatization of $\infty$-groupoids.  By a "metatheory of Book HoTT" I would understand a description of the syntax of Book HoTT, sufficient to prove statements like "$\mathbb{N} \equiv \mathbb{Z} : \mathscr{U}$ is not derivable", and to state and prove the interpretability of that syntax in appropriate categories.  Such a metatheory certainly exists: lots of people study metatheory of type theories.
By contrast, by a "first-order axiomatization of $\infty$-groupoids", I would understand a theory in first-order logic, like ZFC, whose models are "universes of $\infty$-groupoids" in the same way that the models of ZFC are "universes of sets".  My best guess at the connection you have in mind would be a first-order theory whose models are the models of Book HoTT, regarded as small categories inside $\rm Set$ the same way a model of ZFC is a single object of $\rm Set$ with a relation on it.  In other words, the first-order theory of a category with families, or some variant thereof, with all the additional type structure corresponding to Book HoTT.  Is this the sort of thing you have in mind?
Edit: Based on the comments, let me add a bit more about how this latter thing is and isn't what you might have in mind.  On the one hand, this is a way to specify, if you insist on working in an ambient first-order logic, a structure that corresponds roughly to a dependent type theory such as Book HoTT.
However, because of the differences I explained above, formulating such a theory inside FOL and then working in it would not really be analogous to formulating ZFC inside FOL and then working in it.  It would be more like formulating the notion of "model of ZFC" inside FOL.  Normally when we work in ZFC, the notion of "proposition" we use is the one from the ambient FOL, with no other choice; but if instead we formulated "model of ZFC" in FOL then there would be two different notions of "proposition", the ambient one and the one pertaining to the model.  The one you would want to use is the one pertaining to the model, so in essence you wouldn't really be using the ambient FOL you started from, and it would be a tedious translation to add an extra layer of indirection to everything
Similarly, if you formulate the first-order theory of a CWF, you'll end up with two notions of "proposition": the ambient one of the FOL, and the internally defined propositions-as-types notion of the DTT of the CWF.  The latter is the one you want to use, so you wouldn't actually be using the ambient FOL much, and you'd again have the tedious layer of indirection.  If you want to work with Book HoTT, it's much better to implement it directly as a deductive system than try to talk about its models inside FOL.
A different question is whether there is a "first-order theory of $\infty$-groupoids" that could be formulated inside FOL without indirection, analogously to ZFC.  I don't think anyone has succeeded in writing down such a thing, and I'm dubious that it is possible, because the identification of propositions with certain types seems crucial to the way HoTT works, whereas breaking off the propositions into a separate level of FOL seems like it would prevent that.  But I don't have a watertight argument against it.
