拡張包括構造を持った圏が、カートメル構造／カートメル性〈Cartmell property〉を持つとは、$`\newcommand{\cat}[1]{\mathcal{#1}}`$
- |$`\cat{C}`$| 上の長さ関数 $`\ell :|\cat{C}| \to {\bf N}`$ がある。
- 長さが 0 の対象は終対象に限る。終対象はひとつしかない。
- $`\ell(\Gamma\cdot A) = \ell{\Gamma} + 1`$
- 正の長さの $`\Gamma\in |\cat{C}|`$ に対して、$`\Gamma = \Gamma'\cdot A`$ となる $`\Gamma'`$ が一意に存在する。
カートメル性を持つ属性付き圏〈category with attributes〉やファミリー付き圏〈category with families〉をコンテキスト圏またはCシステムと呼ぶ。ボエボドスキーのCシステムはカートメル属性付き圏〈Cartmellian category with attributes〉。
拡張包括構造、または単に包括構造は：
- インデックス付き圏＝ファイバー付き圏＝ファイブレーション
- 拡張演算（データ）
- 拡張の射影（データ）、拡張＋射影で広義の拡張。広義の拡張は、$`\cat{C}`$ 上の圏バンドルのデカルト関手
- 射影のリダクト関手＝移行関手〈transfer functor〉（データ）
- 射影達がディスプレイクラス〈ファイバー引き戻し安定クラス〉になること。（法則・性質）
- [引き戻し公理] ディスプレイ引き戻し図式が、拡張演算と移行関手で書けること。（法則・性質）
