Awodey, later with Newstead, showed how polynomial functors with extra structure (termed ``natural models'') hold within them the categorical semantics for dependent type theory. Their work presented these ideas clearly but ultimately led them outside of the usual category of polynomial functors to a particular \emph{tricategory} of polynomials in order to explain all of the structure possessed by such models. This paper builds off that work -- explicating the categorical semantics of dependent type theory by axiomatizing them entirely in terms of the usual category of polynomial functors. In order to handle the higher-categorical coherences required for such an explanation, we work with polynomial functors in the language of Homotopy Type Theory (HoTT), which allows for higher-dimensional structures to be expressed purely within this category. The move to HoTT moreover enables us to express a key additional condition on polynomial functors -- \emph{univalence} -- which is sufficient to guarantee that models of type theory expressed as univalent polynomials satisfy all higher coherences of their corresponding algebraic structures, purely in virtue of being closed under the usual constructors of dependent type theory. We call polynomial functors satisfying this condition \emph{polynomial universes}. As an example of the simplification to the theory of natural models this enables, we highlight the fact that a polynomial universe being closed under dependent product types implies the existence of a distributive law of monads, which witnesses the usual distributivity of dependent products over dependent sums.

翻译：Awodey 及后来与 Newstead 合作的研究表明，具有额外结构的多项式函子（称为“自然模型”）包含了依赖类型论的范畴语义。他们的工作清晰地阐述了这些思想，但最终引导他们走出了通常的多项式函子范畴，进入了一个特定的多项式\emph{三范畴}，以解释此类模型所具备的全部结构。本文基于该工作展开——通过完全依据通常的多项式函子范畴来公理化依赖类型论的范畴语义，从而阐明其语义。为了处理此类解释所需的高阶范畴连贯性，我们在同伦类型论（HoTT）的语言框架下研究多项式函子，这使得高阶结构能够纯粹在该范畴内表达。此外，转向 HoTT 使我们能够表达多项式函子的一个关键附加条件——\emph{单值性}——该条件足以保证，表达为单值多项式的类型论模型，仅凭其在依赖类型论的通常构造子下封闭这一性质，就能满足其相应代数结构的所有高阶连贯性。我们将满足此条件的多项式函子称为\emph{多项式宇宙}。作为这种方法对自然模型理论的简化示例，我们强调一个事实：一个多项式宇宙在依赖积类型下封闭，意味着存在一个单子分配律，这体现了依赖积对依赖和的通常分配性。