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.

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