We develop the usage of certain type theories as specification languages for algebraic theories and inductive types. We observe that the expressive power of dependent type theories proves useful in the specification of more complicated algebraic theories. We describe syntax and semantics for three classes of algebraic theories: finitary quotient inductive-inductive theories, their infinitary generalization, and finally higher inductive-inductive theories. In each case, an algebraic signature is a typing context or a closed type in a specific type theory.

翻译：我们发展了某些类型的理论的使用,作为代数理论和感官学类型的具体语言。我们观察到,依赖型理论的表达力证明有助于更复杂的代数理论的具体说明。我们描述三类代数理论的语法和语法:有线感感性感性理论、其无止境的概括性理论、以及最后更高的感性感性感性理论。在每一种情况下,代数签字都是一种打字背景或特定类型理论中的一种封闭类型。