Awodey, later with Newstead, showed how polynomial pseudomonads $(u,1,\Sigma)$ with extra structure (termed "natural models" by Awodey) hold within them the categorical semantics for dependent type theory. Their work presented these ideas clearly but ultimately led them outside of the category of polynomial functors in order to explain all of the structure possessed by such models of type theory. This paper builds off that work -- explicating the categorical semantics of dependent type theory by axiomatizing them \emph{entirely} in the language of polynomial functors. In order to handle the higher-categorical coherences required for such an explanation, we work with polynomial functors internally in the language of Homotopy Type Theory, which allows for higher-dimensional structures such as pseudomonads, etc. to be expressed purely in terms of the structure of a suitably-chosen $\infty$-category of polynomial functors. The move from set theory to Homotopy Type Theory thus has a twofold effect of enabling a simpler exposition of natural models, which is at the same time amenable to formalization in a proof assistant, such as Agda. Moreover, the choice to remain firmly within the setting of polynomial functors reveals many additional structures of natural models that were otherwise left implicit or not considered by Awodey \& Newstead. Chief among these, we highlight the fact that every polynomial pseudomonad $(u,1,\Sigma)$ as above that is also equipped with structure to interpret dependent product types gives rise to a self-distributive law $u \triangleleft u\to u \triangleleft u$, which witnesses the usual distributive law of dependent products over dependent sums.

翻译：Awodey（后来与Newstead合作）证明了具有额外结构（被Awodey称为“自然模型”）的多项式伪幺半群$(u,1,\Sigma)$包含了依值类型理论的范畴语义。他们的工作清晰地阐述了这些思想，但最终为了解释此类类型理论模型所具备的全部结构，不得不脱离多项式函子的范畴。本文基于该工作，通过完全用多项式函子的语言公理化依值类型理论的范畴语义来阐释其结构。为了处理此类解释所需的高维范畴连贯性，我们在同伦类型理论的语言内部处理多项式函子，这使得伪幺半群等高维结构能够纯粹通过适当选取的多项式函子$\infty$-范畴的结构来表达。从集合论转向同伦类型理论因此产生双重效果：既使得自然模型的阐述更为简洁，又便于在Agda等证明助手中形式化。此外，坚持严格保持在多项式函子框架内的选择，揭示了Awodey & Newstead工作中原本隐含或未考虑的许多自然模型附加结构。其中最重要的是，我们强调每一个如上所述且配备了解释依值积类型结构的多项式伪幺半群$(u,1,\Sigma)$，都会产生一个自分配律$u \triangleleft u\to u \triangleleft u$，该分配律见证了依值积对依值和的经典分配律。