拡張包括構造については、「最近の型理論： 拡張包括構造を持ったインデックス付き圏」で述べたことがあります。型理論的圏（「指標の圏はコンテキストの圏の反対圏」参照）は、なんらかの拡張包括構造を持ちます。拡張包括構造の定式化は色々とあります。ジ…