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.

翻译：我们发展了将特定类型理论作为代数理论与归纳类型规范语言的使用方法。我们观察到依赖类型理论的表达能力在更复杂代数理论的规范化中展现出实用价值。我们描述了三类代数理论的语法与语义：有限商归纳-归纳理论、其无穷推广，以及高阶归纳-归纳理论。在每种情形中，代数签名都是特定类型理论中的类型化上下文或封闭类型。