Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. For example, the theories of categories or Martin-L{ö}f type theories form GATs. Categories have two sorts, objects and morphisms, and the latter are double-indexed over the former. Martin-L{ö}f type theory has four sorts: contexts, substitutions, types and terms. For example, types are indexed over contexts, and terms are indexed over both contexts and types. In this paper we show that any GAT can be reduced to a GAT with only two sorts, and there is a section-retraction correspondence (formally, a strict coreflection) between models of the original and the reduced GAT. In particular, any model of the original GAT can be turned into a model of the reduced (two-sorted) GAT and back, and this roundtrip is the identity. The reduced GAT is simpler than the original GAT in the following aspects: it does not have sort equalities; it does not have interleaved sorts and operations; if the original GAT did not have interleaved sorts and operations, then the reduced GAT won't have operations interleaved between different sorts. In a type-theoretic metatheory, the initial algebra of a GAT is called a quotient inductive-inductive type (QIIT). Our reduction provides a way to implement QIITs with sort equalities or interleaved constructors which are not allowed by Cubical Agda. An instance of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Our approach is semantic in that it does not rely on a syntactic description of GATs, but instead, on Uemura's bi-initial characterisation of the category of (finite) GATs in the 2-category of finitely complete categories with a chosen exponentiable morphism.

翻译：广义代数理论（GAT）允许多种类型相互索引。例如，范畴论或Martin-Löf类型理论构成GAT。范畴论具有两种类型：对象和态射，后者在前者上双重索引。Martin-Löf类型理论具有四种类型：上下文、替换、类型和项。例如，类型在上下文上索引，而项同时在上下文和类型上索引。本文证明任何GAT均可约化为仅含两种类型的GAT，且原GAT与约化GAT的模型之间存在截面-收缩对应关系（严格形式为严格余反射）。特别地，原GAT的任何模型均可转换为约化（双类型）GAT的模型并还原，此循环变换为恒等映射。约化GAT在以下方面较原GAT更简化：不包含类型等式；不包含交错排列的类型与运算；若原GAT本无交错排列的类型与运算，则约化GAT亦不会出现不同类型间的交错运算。在类型理论的元理论中，GAT的初始代数称为商归纳-归纳类型（QIIT）。本约化方法为在Cubical Agda中实现那些不允许包含类型等式或交错构造子的QIIT提供了途径。该约化的一个实例是将互归纳类型约化为单一索引族的经典方法。本方法具有语义学特性：不依赖GAT的语法描述，而是基于上村在具有可指数态射的有限完备范畴的2-范畴中，对（有限）GAT范畴的双始刻画的表征。