前置き
ここでも言いますが、はじめにでも述べているように、このサイトの製作者（算散士）は 型理論をあまりよく知りません。 ですから、本格的に知りたい人は他をあたった方がいいと思います。
型付きλ式
さて、ここで型付きλ式の厳密な定義．．．と行きたいところなのですが、結局は 私自身よくわかっていません。λ-cubeあたりまでは、あたってみたのですが、Coqは CC（Calculus of Constractions）とも違って CIC（Calculus of Inductive Constructions）というらしく、今、リファレンス マニュアルやCoq'Artに一生懸命アタックしているところです。 （もっとわかりやすい文献ありましたら、どうか こちらにでも情報提供よろしくお願い致します。）
それに、今ここで必要なのは、Print命令で表示されるλ式から証明を読み取る ことができればいいだけなので、とりあえずはそれに必要な説明だけをここで試み ようと思います。
では、型付きλ式を大雑把に説明しましょう。とてもとても大雑把に 言うなら、型のないλ式の各変数に型を付け加えたもの、ということになるで しょうか。 型のないλ式のページの１．２．３．に対応して、 もう少し表記や型の付き方について詳しく言うと、
上記１．２．３．のイメージをお話しましょう。 型付きλ式Ｍが型Ａを持っている場合、 Ｍ：Ａ と表記しますので、 以下その表記を使います。
ここではイメージというより、ｘ：Ａなる表記の別の見方を紹介します。 それは集合のような見方です。ｘ：Ａと表記したとき、これはｘが型Ａを持つ という意味なのですが、もし、型Ａを持つもの全てを集めた集合もＡで表記 するなら、ｘ：Ａは、「ｘは集合Ａの要素である」とも読めます。以下、このような 見方もしますので覚えておいてください。
（λｘ：Ａ．Ｍ） は、型のないλ式のときと同様、（型がＡである）変数ｘ を引数とする関数のイメージです。一般には、 Ｍ も Ｂ も自由変数としてｘを含 んでいますので、それを強調するために、 Ｍ（ｘ）、Ｂ（ｘ） と表記して もう一度復習してみましょう。Ｍ（ｘ） の型は Ｂ（ｘ） ですから、
と表記され、これをｘの関数としてみた （λｘ：Ａ．Ｍ（ｘ）） の 型は Πｘ：Ａ．Ｂ（ｘ） なので、
と表記されます。ということで、上記ｂ．のイメージを言葉で言うと
です。ここで、たまたま型 Ｂ が自由変数ｘを持っていなかった場合を考えま しょう。つまり、型 Ｂ がｘに依存しないわけです。この場合に上記ｃ．を 考えてみると、まるで、「集合Ａ（というより、型Ａであるものを全て集めた集合） から集合Ｂ（型Ｂであるものを全て集めた集合）への関数（写像）」を述べている ように見えます。それで、この場合に限り、上記ｂ．は
と略記されます。つまり、 （λｘ：Ａ．Ｍ（ｘ）） は Ａ から Ｂ への 関数である、というわけです。逆に、ｂ．はｄ．を少し一般化したもの、という 見方をすると少しわかりやすいかもしれません。（集合と写像の知識のない人は、 たまたま型 Ｂ が自由変数ｘを持っていない場合は、ｄ．のように略記するという ことだけ覚えておいてください。）
ここで、上記の１．と２．のイメージ をあわせて、ｆ：Ａ→Ｂを読み取ってみましょう。 もちろんこれは「ｆは型Ａ→Ｂを持つ」と読むことができます。さて、１．で 話したように、Ａ→Ｂは、型Ａ→Ｂを持つもの全体の集合とも読むことにします。 そして型Ａ→Ｂとは、ＡからＢへの関数（写像）を表す型ですから、結局、 Ａ→Ｂは、ＡからＢへの関数（写像）全体の集合ということになります。 再び１．のイメージの説明を思い出してｆ：Ａ→Ｂを読み取ると、 「ｆはＡからＢへの関数（写像）全体の集合の要素である」つまり、 「ｆはＡからＢへの関数（写像）である」ということになります。
まったく同様にｇ：Ａ→（Ｂ→Ｃ）を読み取るとどうでしょう。今の段階では 「ｇはＡからＢ→Ｃ（ＢからＣへの関数全体の集合）への関数である」としか 言えませんが、いずれ2変数関数とみなせる話をします。
今度は、Ｍが型Πｘ：Ａ．Ｂの型付きλ式ですから、Ｍは
のような形をしているはずです。つまり Ｍ は、（また、Ｂ も Ｂ（ｘ） のように 表記します。）
というイメージを持った型付きλ式です。そして、（ＭＮ）は 型のないλ式のページの３．とまったく同様な イメージで、
というイメージのものです。とすれば、（ＭＮ）の型は当然
になります。これは Ｂ（Ｎ） と書き表してもいいでしょうし、上記３． では Ｂ［ｘ：＝Ｎ］ と表記しました。
ちなみに、 Ｂ が自由変数ｘを持っていない場合、（このとき、 Ｍ の型 は Ａ→Ｂ と略記されますが、） Ｂ［ｘ：＝Ｎ］ は Ｂ とまったく同じに なります。（Ｂ の中に代入すべき場所がないからです。）
ちょっと論理
上記３．の Ｍ：（Πｘ：Ａ．Ｂ） において、型Ｂが自由なｘを持っていない 場合、 Ｍ：（Ａ→Ｂ） となるわけですが、これと Ｎ：Ａ から、 （ＭＮ）：Ｂ を 作る様子を次のように図にして見ましょう。
|
Ｍ：（Ａ→Ｂ） |
Ｎ：Ａ |
|
------------------------ |
|
|
（ＭＮ）：Ｂ |
|
上記 ｉ． の、型のところだけ見てください。Ａ→Ｂ と Ａ から Ｂ を 導いています。これは論理の、いわゆるmodus ponensと呼ばれる推論 です。このように、 型付きλ式の構成は、推論の積み重ねにも見ることができるのです。
Coqでの表記
Coqでは、型付きのλ式の関数抽象の部分が少し違った表記になります。 つまり、 （λｘ：Ａ．Ｍ） なるλ式は
ｆｕｎ （ｘ：Ａ） ＝＞ Ｍ
と表記されます。また、省略形と して、 （λｘ：Ａ．（λｙ：Ｂ．Ｍ）） なるλ式は
ｆｕｎ （ｘ：Ａ） （ｙ：Ｂ） ＝＞ Ｍ
と表記されます。さらに型 Ａ と型 Ｂ が同じときは
ｆｕｎ （ｘ ｙ：Ａ） ＝＞ Ｍ
と表記されます。
また、変数ｘの型が Ａ のとき、原則として ｘ：Ａ と 表記するのですが、他の部分で既に ｘ：Ａ なる表記があって、繰り返し 型を表示する必要のないときは、単にｘと表記されます。
さらに、型の Πｘ：Ａ．Ｂ のCoqでの表記は
ｆｏｒａｌｌ ｘ：Ａ，Ｂ
となります。ＡとＢの間にあるのは「，」（コンマ）なので気をつけて
ください。
また、λ式のときと同様、省略形として、
（Πｘ：Ａ．（Πｙ：Ｂ．Ｃ）） なる型は
ｆｏｒａｌｌ （ｘ：Ａ） （ｙ：Ｂ），Ｃ
と表記されます。さらに型 Ａ と型 Ｂ が同じときは
ｆｏｒａｌｌ ｘ ｙ：Ａ，Ｃ
と表記されます。
結局、上記ｂ．の（λｘ：Ａ．Ｍ（ｘ））：（Πｘ：Ａ．Ｂ（ｘ））は、Coqの表記 の仕方では
（ｆｕｎ （ｘ：Ａ） ＝＞ Ｍ（ｘ））：（ｆｏｒａｌｌ ｘ：Ａ，Ｂ（ｘ））
となります。
1変数関数と多変数関数の型
また、ふつうのλ式の記法で話を続けます。 型のないλ式で、 2変数の話をしました。 そこで言いたかったのは、λ式の記法では1変数の関数の表現方法しか定義されて いないのに、工夫によって多変数もあつかうことができるということでした。 もちろん、型付のλ式においても同様な工夫ができます。
多変数であれば同様なので、2変数で話を続けます。さて、2変数ですから、 例えば Ａの要素ａと、Ｂの要素ｂを与えると、Ｃの要素がただひとつ定まる関数ｇを 今までの方法で表現してみましょう。それは上記でも軽く触れた ｇ：Ａ→（Ｂ→Ｃ）です。次を見てください。（上記「 １．のイメージ」の説明に従うと、「Ａの要素ａ」などと 言うときは、「ａ：Ａ」と表記すれば事足りる。）
つまり、ｇ：Ａ→（Ｂ→Ｃ）を使えば、ａ：Ａとｂ：Ｂからｇａｂ：Ｃを 作れるわけです。集合論の書き方に従えば、ｇはｇ：Ａ×Ｂ→Ｃとなり、ｇａｂは ｇ（ａ，ｂ）となるでしょうか。
同様に、Ａ、Ｂ、Ｃの各要素を与えるとＤの要素が定まる3変数関数ｈの 型は、ｈ：Ａ→（Ｂ→（Ｃ→Ｄ））となります。「→」が右に結合的であること から、ｈ：Ａ→Ｂ→Ｃ→Ｄと括弧を省略することもできます。