型の導入規則とは、型の生成規則で、型だけではなくて要素の構成規則も含む。
- 型を型構成子で生成する。
- 要素を要素〈値〉構成子で生成する。要素生成子は関数である。
型の除去規則とは、型の消費規則で、関数による要素の構成規則（「構成」で間違ってない）も含む。
- 既に型構成子で生成した型と要素がある。
- その型の要素に関数を後結合子て消費すると、中間の型を除去した（カットした）要素が得られる。
次のようにも言える。
- 導入規則は、複合型を域とする関数の構成法を与える。当該複合型の新しい証拠を生成する。
- 除去規則は、複合型を余域とする関数の構成法を与える。当該複合型の既存証拠を消費して、新しい証拠を作る。
- 複合型には、アロー型、依存アロー型、直積型〈タプル型〉、直和型〈タグ付きユニオン型〉、一般的帰納的型がある。
- 一般的帰納的型の導入規則と除去規則は難しくなる。簡単な例はタグ付きユニオン型の、値コンストラクタとパターンマッチ分岐処理。
規則はコンビネータであり、そのコンビネータを使うコマンドでもある。また、関数は後結合／前結合でコンビネータとみなすことができる。And.intro は関数だが、And.introを後結合するコンビネータ doPostComp And.intro でもあり、コンビネータを入力シーケントに適用するコマンドでもある。
