型理論的形式体系〈type-theoretic formal system〉とは、抽象的演繹系（「演繹系とオペラッド」参照）の一種で、基本的な構文構成素としてコンテキストと何種類かの判断を持ちます。
型理論的形式体系があると、コンテキストを対象として、コンテキストのあいだの代入〈substitution〉（の判断）を射とする圏を構成できます。これを、型理論的形式体系の構文圏〈{syntax | syntactic} category〉と呼びます。構文圏として色々な種類の圏が提案されています。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\hyp}{\text{－} }`$
- 包括圏〈comprehension category〉
- ファミリー付き圏〈category with families | CwF〉
- 局所デカルト閉圏〈locally Cartesian closed category | LCCC〉
- 属性付き圏〈category with attributes | CwA〉
- ディスプレイクラス付き圏〈category with display maps | CwD〉
- C-システム〈C-system〉（属性付き圏 ＋ カートメルツリー構造）
「球体集合達の圏の構文表示 1/2」において、形式体系達の集合から、小さい圏または大きい〈小さいとは限らない〉圏を作り出す手続きとして $`\mrm{SynCAT}(\hyp)`$ を導入しました。$`\mrm{SynCAT}(\hyp)`$ への引数は型理論的形式体系で、結果として型理論的圏が構成されます。
型理論的形式体系として、一般化代数セオリー〈generalized algebraic theories | GATs〉の形式体系などを考えてみると、構文“圏”とは限らず、もっと一般的な代数構造を考える必要がありそうです。なので、$`\mrm{SynCAT}(\hyp)`$ を $`\mrm{SynAS}(\hyp)`$ に変更します。AS は Algebraic System の頭文字〈イニシャリズム〉です。
では、なんらかの形式体系 $`S`$ から作られた $`\mrm{SynAS}(S)`$ はどんな代数系となるのでしょう？ もちろん圏になる場合もあります。多くの場合、単なる圏ではなくて（明示的ではなくても）ファイバー付き圏の構造を持ちます。幾つかの事例を見ると、確かにファイバー付き構造を持ってはいますが、ベースもファイバーも圏ではないことがあります。複圏〈multicategory | オペラッド〉や多圏〈polycategory〉が出てきます。さらに、通常の複圏・多圏よりも複雑なシロモノが出てきます。
通常の複圏の場合、複射〈multimorphism | operator | operation〉の域〈ソース側〉は色〈対象〉のリストです。非対称（対称性を持たない）複圏であっても、リストであることに変わりはありません。ところが、依存型理論では依存リストを扱うので、複射の域に（多射の場合は余域にも）依存リストが現れます。実際には、複圏が埋め込まれた多圏を扱うことになり、ファイバー付き構造のベースもファイバーも依存多圏（域・余域が依存リストである多射達の代数系）なのです。
ファイバー付き依存多圏〈fibered dependent polycategory〉は一般性がある代数系なので、型理論的形式体系の構文代数系として利用されてきた既存の代数系〈代数構造〉をだいたい包摂できると思います。ファイバー付き依存多圏は、型理論的形式体系の構文構造を表す代数系なので、すべての構成素が帰納的〈inductive〉な構成法で生成されることが重要です。
C-システムにおけるカートメルツリー構造のように、構成素がどのような経緯・歴史を辿って今に至るのかをトレースできる構造が欲しいのです。このテの履歴情報は、意味論的には不要、むしろ邪魔な夾雑物ですが、構文論とは、夾雑物（言い回しの違い）込みで定式化するものだと思います。
