γアノテーション（ガンマ項）の構文的な特徴

γアノテーションは、束縛子や限量子と似た構文で、γ記号の後に変数を伴いスコープを持つ。γにくっついている変数をγ変数と呼ぶことにする。

γアノテーションに変数の束縛作用はなくて、γアノテートされた項（スコープ内部）でγ変数は自由のままである。したがって、γ変数はリネーム作用（アルファ変換）の影響を受ける。リネームに関してγ変数は単なる自由変数だが、置換に対しては特殊な働きをする。

• γ変数を置換できるのはラムダ抽象の形をした項に限る
• γ変数を通常の単純置換で置換することはできない。γ置換を使う。

∀や∃では、vacuous quantificationってのがあるけど、γアノテーションがvacuousのときは、アノテーション自体を削除してもよい。つまりは、γ変数が自由に出現してない項に対するγアノテーションは無視される。γアノテーションが、特殊な置換を指示するマーカーであることを考えると当たり前だ。

γアノテーションは構文的な方便であって、意味はあくまでも指数関手（累乗関手というほうが適切か）。