多项式向量（类型理论）

在类型理论中，多项式向量（或容器向量）是一种类型类别的内向量，与归纳和共轭类型的概念密切相关。具体来说，所有的W类型（resp.M类型）都是（同构于）这种漏斗的初代库（resp.终代库）。多项式向量已经在带有Σ-类型的预设中被研究过了；这篇文章只涉及这个概念在马丁-洛夫式类型理论的类型范畴内的应用。

让U是一个类型的宇宙，让A：U，让B：A→U是一个由A索引的类型族。与容器（A，B）相关的多项式向量定义如下。任何与P自然同构的漏斗都被称为容器漏斗。P对函数的作用被定义为注意，这个赋值不仅在扩展类型理论中是真正的放克性的（见#属性）。

在扩展类型理论中，这样的函数不是真正的向量，因为宇宙类型严格来说不是一个范畴（同构类型理论领域致力于探索宇宙类型如何表现得更像一个高等范畴）。然而，在命题等价的前提下，它是放克性的，也就是说，以下身份类型是居住在其中的。{displaystyle{mathsf{id}}_{X}}是类型X上的同一函数。是类型X上的同一函数。