指標と項の次元

• 型／ソート変数（型／ソート名）は、0-項。0-生成元＝0-セル
• 型項は、0-項。生成された0-射
• 定数／変数は、1-項。1-生成元＝1セル。点射または域不定射
• 値項は、1-項。1-射だが、点射
• 関数項は、1-射。一般の射、または、フルカリー化された点射

項の構成法

• 型項は型構成子で作る。型構成子は関手の結合。
• 値項は値構成子で作る。値構成子は射の後結合か圏論的コンビネータ。
• 関数項は関数構成子で作る。関数構成子は圏論的コンビネータ
• 命題項〈論理式〉は命題構成子で作る。命題項は関数項の一種。
• 等式は、公理等式と等式推論のコンビネーション。