The HoTT book says:
We will not attempt to give a formal presentation of the grammar of a valid inductive definition and its resulting induction and recursion principles and pattern matching rules. This is possible to do (indeed, it is necessary to do if implementing a computer proof assistant), but provides no additional insight. With practice, one learns to automatically deduce the induction and recursion principles for any inductive definition, and to use them without having to think twice.
So I'm on the lookout for an EBNF or PEG grammar that describes the syntax of everything in HoTT book. Is there one out there? Is it even possible to write one down? Because I got stuck implementing $\mathcal{U}_i$ (the $i$th universe) as a class in Python. Since $i:\Bbb{N}$ yet $\Bbb{N}: \text{Type}$ and $\text{Type} : \mathcal{U}_i$ for some $i$. So what you get is a circular import error that is AFAICT not possible to get rid of.
So a grammar might lend some advice on structuring the Python encoding of the theory as well.