在類型理論中，容器是一種抽象，它允許各種集合類型，如列表和樹，以統一的方式表示。容器的擴展是由一個形狀（S型）和一個位置（P型）組成的依賴對家族，其中包括一個形狀（S型）和一個從該形狀的位置到元素類型的函數。容器可以被看作是集合類型的典范形式。對于列表，形狀類型是自然數（包括零）。相應的位置類型是小于形狀的自然數的類型，對于每個形狀。對于樹，形狀類型是單位的樹的類型（也就是沒有信息的樹，只有結構）。對應的位置類型與每個形狀的從根到形狀上的特定節點的有效路徑類型是同構的。請注意，自然數與單位列表是同構的。一般來說，形狀類型將總是與應用于單元的原始非通用容器類型系列（列表、樹等）同構。引入容器概念的主要動機之一是在依賴類型的環境中支持通用編程。

容器的擴展是一個endofunctor。它把一個函數g帶到在列表的情況下，這相當于我們熟悉的映射g，對其他容器也有類似的作用。

索引型容器（也被稱為依賴多項式向量）是容器的一種概括，它可以表示更廣泛的類型，比如向量（大小的列表）。元素類型（稱為輸入類型）是由形狀和位置來索引的，所以它可以因形狀和位置而變化，而擴展（稱為輸出類型）也是由形狀來索引的。