LaTeX pretty-printing of GATs

Pretty-print GATs as LaTeX in both of the following styles:

1. Cartmell-style linear notation

2. natural-deduction-style tree notation

The examples above depict the theory of monoids and are taken from Sterling's paper [Algebraic type theory and universe hierarchies](https://arxiv.org/abs/1902.08848).

The first style is similar to the syntax of our `@theory` macro and should be easily ported to MathJax/KaTeX, while the second style is harder to typeset but beloved by type theorists.