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{多项式宇宙}。作为此方法对自然模型理论简化的例证，我们强调一个事实：多项式宇宙在依赖积类型下封闭意味着存在单子分配律，这见证了依赖积对依赖和的通常分配性。