让下一篇重要论文，不再错过。

原文摘要

Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. 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 involving only two sorts: a first one without dependencies, and another one indexed over the former. We show that a model of the reduced GAT is equivalently given by a pair consisting of a model of the original GAT, which we call the core model, and a "cartesian" morphism from the family of sets induced by this core model. In a type-theoretic metatheory, the initial model of a GAT is called a quotient inductive-inductive type (QIIT). The above characterisation justifies soundness of the reduction, in the sense that the QIIT of the original GAT can be simulated from the QIIT of the reduced GAT, by taking its core model. A particular case of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Other instances of this reduction can be found in the literature to simulate sophisticated QIITs in Cubical Agda. Indeed, 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. 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.