12/02/05 21:21:15.51
何を言っているのかさっぱり分かんない…
ちょっと気まぐれで覗いてみたが、まるで地獄だ…
532:１３２人目の素数さん
12/02/05 21:24:59.11
>>522
>流行るかどうかがやっぱり最も大事じゃないの？
そもそも基礎論自体が流行っていないｗｗ
集合論が圏論より流行ってると言っても団栗の背比べｗｗｗ
533:１３２人目の素数さん
12/02/05 21:42:26.99
>>527
へたに柔らかく言い過ぎたか？
そんな圏論ならそんなふうにニッチにやっていけばいい。
だが圏論にはもっと大きな意味があると聞こえているので、もしそうなら衆人にそれが分かるように
言ってくれと言った。
>>528
だって公理の数の件は数えるものが悪いだけだね？
それくらいあなたにも分かっているだろと思うから。
>>529
528とも同じくいまは本質的なことじゃないと思うのでごめん。
534:スレタイスレ446
12/02/05 21:46:45.82
>>530
URLﾘﾝｸ(citeseerx.ist.psu.edu)
私に探せるものであなたに探せないものはない。
535:１３２人目の素数さん
12/02/05 21:58:06.95
＞圏論にはもっと大きな意味があると聞こえているので
こういう誤解をする人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場
536:スレタイスレ446
12/02/05 22:01:36.30
URLﾘﾝｸ(www.springerlink.com)
>>530
申し訳ないが読んだことがない本で・・・。
537:１３２人目の素数さん
12/02/05 22:10:19.25
>>533
>そんな圏論ならそんなふうにニッチにやっていけばいい。
そんなふうがニッチと思うかどうかは結局主観の問題だからね。
「集合論の問題はニッチなものだけじゃない」と何人かの専門家が解説しているのを見てきたけど、
ほとんどの部外者には「なんだ、やっぱりニッチな話じゃん」としか思わないだろうし。
ニッチかどうかなんてそんなもんよ。
538:１３２人目の素数さん
12/02/05 22:14:10.18
>535 これは必ずしも誤解ではなく、たしかに昔からよく耳にするな
539:１３２人目の素数さん
12/02/05 22:20:50.39
>>537
客観性のない主観的な罵り言葉なんて、負け惜しみの捨て台詞なんだから生暖かくスルーしてやればよろし。
540:１３２人目の素数さん
12/02/05 22:32:07.80
>>538
「もっと大きな意味」とか曖昧な言葉を含んでいるものに
「誤解ではなく」とか断言できる神経が全く理解できないな。
541:１３２人目の素数さん
12/02/05 22:40:37.13
>>540
まさか圏論の近くにはこんな人が多いんじゃないだろなｗ
542:１３２人目の素数さん
12/02/05 22:48:13.06
低俗な煽り合いはもう終了でいい？
もっと生産的な話がしたくてさっきから待ってるんだけど。
>>513
圏論に対応させる形式体系として型理論の方がよく出てくるのは確かにそおの通り。
だけど、圏論をそのまま一階述語論理にのっける公理系も Lwavere を始め研究されている。
最近でも以下のような論文が出ている。最近つっても10年以上前だけど。
URLﾘﾝｸ(www.cwru.edu)
543:１３２人目の素数さん
12/02/05 23:06:11.24
>538,541
そこまで言うのなら「よく耳にする」で済ませないで、
出典を明らかにするなりリンク貼るなりすれば？
そうすれば「低俗な煽り合い」と言われないで済むと思うけど。
544:１３２人目の素数さん
12/02/05 23:41:57.51
>>529
A∧BよりAの方が短い、という意味では公理系の極小性は定義できない？
もちろん、Aと全然違うCとどちらが小さいとも言えないから
集合論と圏論の比較には役に立たないだろうけどさ。
545:１３２人目の素数さん
12/02/06 01:01:17.41
>>526,>>533
数学の基礎付け・形式化に、集合論は必須のものなのか、
それとも別の方法も可能だけど歴史的経緯や使いやすさで集合論が選ばれているだけなのか、
という問題は重要な問題だと思う。
だから「集合論もあるけどこれもある」っていう圏論の研究は意味があるし、全くニッチな研究だとは思わない。
数学の基礎付け・形式化そのものがニッチだという人には「興味が違うのね」としか言えないけど。
546:１３２人目の素数さん
12/02/06 01:17:56.40
哲オタ乙。研究にどんな意味があるかどうかなんて言い方次第って実例だなｗ
547:１３２人目の素数さん
12/02/06 02:25:02.65
538が言っているのは
「独立した個を重視する西洋近代の終焉が...、これからは関係性を重視した圏論が...」
っていうポモな人たち（いや本当にポモなのかも知らないけど）の発言なんじゃない？
そんなのに踊らされてるなんて...
548:１３２人目の素数さん
12/02/06 03:56:14.39
>>544
＞数学の基礎付け・形式化に、集合論は必須のものなのか、
＞それとも別の方法も可能だけど歴史的経緯や使いやすさで集合論が選ばれているだけなのか
その大事な大事な研究の結果、どっちだと分かったの？少なくとも結論には興味ある。
549:１３２人目の素数さん
12/02/06 06:32:36.80
>>548
横レスかもしらんが、型理論型理論と言ってるように、
型理論で形式化できるものは圏論を使って形式化できる。
「通常の数学」はこの範囲。しかし「通常ではない数学」が問題。
集合論でも圏論が形式化できるかが色々微妙なように、
逆に圏論での形式化では集合論的な数学が問題になる。
特に置換公理が型理論（よって圏論）とは相性が悪いので、
このスレか関連スレでも何度か話題になっているように
置換公理を使った数学（要するに集合論的な数学）をどう評価するべきかという問題になる。
550:１３２人目の素数さん
12/02/06 07:10:13.30
集合論派は「群全体のなす圏、環全体のなす圏などは集合論で記述できないがそんなのは数学の中でごく例外的」と言い、
圏論派は「置換公理を使うような数学は圏論では記述できないがそんなのは数学の中でごく例外的」と言うわけですね。
お互い自分に都合がいいように「数学」というものを設定していると。
551:１３２人目の素数さん
12/02/06 07:18:52.67
>>531
何が地獄なの？？
552:１３２人目の素数さん
12/02/06 07:32:15.44
>>550
そうやって党派的な図式にするのは楽しいのだろうが
>>549は「どう評価するべきかという問題になる」と至って中立的なことしか言っていないぞ
553:１３２人目の素数さん
12/02/06 07:48:24.74
どんな定理に置換公理が必要化はこのスレの上のほうで話題になっていたけど、
そういう背景があったわけね。
554:１３２人目の素数さん
12/02/06 08:26:51.39
亀レスだが>>532が絶妙に本質を突いている件
555:１３２人目の素数さん
12/02/06 17:03:49.97
>>549
型理論に埋め込めるCZFは置換公理を含むんだが？
556:１３２人目の素数さん
12/02/06 19:18:19.50
>>551
文系の俺には全くついていけない別世界、とでも言うかな…
557:１３２人目の素数さん
12/02/06 20:57:01.17
集合論と圏論って、互いに直交していたりしないの？
558:１３２人目の素数さん
12/02/06 21:07:53.82
なんだよ直交って
559:１３２人目の素数さん
12/02/06 21:38:40.59
>>557
そりゃ点（要素）対 矢（射）に象徴されるように直交してるさ。
だがこのスレの大勢的論調では、２つはx軸メインかy軸メインかくらいの
違いしかないらしいんでがっかりしたところだ。
>>558
話が遅いな。少しは推察してやれよ。
560:１３２人目の素数さん
12/02/06 22:49:38.08
>>559
そんじゃおまえがその「直交している」ことの偉大な意義を解説してくれや
561:１３２人目の素数さん
12/02/06 23:01:32.01
トンデモ出現のようだな。基礎論スレの恒例行事。
562:１３２人目の素数さん
12/02/06 23:57:09.75
直交しているという表現を使う>>557は多分プログラマの人なんだろ。
処理系作っていた人がそんな表現使ってた。独立しているぐらいの意味だったはず。
プログラマの人は勝手に変な言葉をあやふやに定義して、形式的に定義された言葉で
みんな知っている、という意味不明な前提を持ち出すから話が成立しない。
563:557
12/02/07 00:16:22.09
>562
そうそう、そんな感じ。
関数空間の基底みたいな話がメタ数学にもあったりしないのかな、と思って。
564:１３２人目の素数さん
12/02/07 00:35:55.15
538=559って要するに、
どこかの哲オタの話を真に受けてゲーデルの不完全性定理には深遠な意味があると勝手に期待したものの、
専門家一同の「ハァ？」を買ってしまって逆ギレ、
という構図だね。
565:１３２人目の素数さん
12/02/07 01:08:20.94
>>563
関数空間に、内積を定義しておかないと、直交も何もないってことは理解できてる？
566:１３２人目の素数さん
12/02/07 01:22:43.08
>>557は
直交しているという言葉にきちんとした意味があるのが
前提になっている書き方だろ
せめて「直交しているみたいな概念がメタ数学にも無いのかな」と言わないと
意味分からん
567:557
12/02/07 01:47:35.76
>565
そういわれてみればそうだね。
プログラムコードなら位相を入れられるけど、集合論と圏論といった概念だとムリなのかなぁ。
568:１３２人目の素数さん
12/02/07 01:57:44.20
>>564
不完全性定理以外にそういうネタがあるってのは新たな発見だったｗ
569:１３２人目の素数さん
12/02/07 03:00:59.43
>>562
＞プログラマの人は勝手に変な言葉をあやふやに定義して、形式的に定義された言葉で
＞みんな知っている、という意味不明な前提を持ち出すから話が成立しない。
変な言葉といえば、ポインタで使われる「指す」という用語の
明示的な定義を未だに見たことが無い。
int a = 0;
int *p = &a;
この場合、「pはaを指す」のか「pはaのアドレスを指す」のか？
ネットを徘徊すると、どっちの使われ方も見かける。
だが、前者の方がより多く使われているように見える。
また、経験上、前者の方がより "正しい" ように思える。
しかし、結局のところ、「指す」の明示的な定義は知らない。
一方で、「代入する」という用語には明示的な定義が用意されていることが多い。
この差は何なのか？
570:１３２人目の素数さん
12/02/07 03:30:24.08
>>569
アドレスを指すというのはもともとは誤用であろう（意味は伝わるが）
アドレスそのものはどこにも無いので指せない。（アドレスが示すメモリはある）
ポインタが指すのはメモリであってアドレスではない。
しかしアドレスというのは住所である。
住所は、実際には土地（場所）を指しているのだが
その土地を住所で代表し、「住所」宛の手紙と言うのと同じ。
つまり、「aを指す」と「aのアドレスを指す」は同じ意味であり
どちらが正しいというものではない。
571:１３２人目の素数さん
12/02/07 03:42:49.95
そもそも 「指す」てのはスラングだわな、だから定義なんかされてない
ポインタがアドレスを保持することを「指す」と言ってるだけで
cそのものの動作に「指す」なんてないわな。
572:１３２人目の素数さん
12/02/07 05:11:52.83
>>570
＞ポインタが指すのはメモリであってアドレスではない。
ところがどっこい、どこかのポインタスレにおいて、
「ポインタが指すのはメモリではなくオブジェクトである。これが分からん奴は半人前だ(ｷﾘｯ」
などと主張する輩がいた。あなたとは正反対の主張だ。
また、>>571によれば「ただのスラング」だそうだ。
これは、あなたの主張とも上記の輩とも違う主張だ。
やはり「指す」は変な用語である。人によって全く見解が違う。
プログラミング業界は、なぜ、「代入する」のように明示的な定義を
早い段階で用意しておかなかったのか？この差は何なのか？
仮に「スラング」が正しいにしても、それならそれで
「指すという用語はスラングである」
という "明示的な定義" が必要である。しかし、このような
定義は広く一般に普及しているとは言い難い。
573:１３２人目の素数さん
12/02/07 05:17:35.35
連投失礼。ちょっと訂正する。
× などと主張する輩がいた。あなたとは正反対の主張だ。
○ などと主張する輩がいた。あなたとは異なる主張だ。
574:１３２人目の素数さん
12/02/07 05:36:09.16
世の中にはソフトリンクもハードリンクもあるのだが
575:１３２人目の素数さん
12/02/07 06:03:05.41
>>572
そういうのを人の褌で相撲を取る、というのだ。
誰かの主張を引用するのなら引用元を明示するべきだろう、
でなければ本当にそういう主張がなされたのか、単なる君の誤解なのか確認するすべがない。
そもそも他人の主張を根拠に何かを批判するのならば、
自分もその主張に賛同する旨を明言するべき。
さもなくば、相手が反論しても「それ、俺の主張じゃないし」と言うのと同じ。
学問的な議論をする際の最低限のルールすら身につけていなかったようだから、
以後気をつけるよーに！
576:１３２人目の素数さん
12/02/07 06:18:34.13
>>572
オブジェクトを指すってのはまたずいぶん抽象的な話だな。
オブジェクトはメモリにのっている。なにも異なる主張ではない。
でなけりゃ void * は何を指しているんだ？
そして「指す」はスラングだと言うのにも矛盾しない。
＞ 「指すという用語はスラングである」
＞ という "明示的な定義" が必要である。
なんで？ そんなもんいらんだろ。
「指す」という語は日本語であるという明示的な定義がなくても
みなが問題なく使用しているように。
577:１３２人目の素数さん
12/02/07 06:28:20.37
>>555
その埋め込みは排中律に適用できない。
つまり直観主義論理でないと成り立たない。
「通常の数学」が排中律を使っていないというのなら、
それに加えて置換公理も含めて圏論で扱える、ということ。
578:１３２人目の素数さん
12/02/07 08:46:49.33
圏論による基礎に関して誰かまとめて下さいませんか？
ぱっと見ただけでも色々な流儀（？）があって、私なりにまとめると以下の通りですが
互いの関係がよく分かりません。
・「集合論が数学の基礎」というのと「基礎」の意味は同じなのか異なるのか、
・述語論理と数学を繋ぐのかそうではないのか、
・型理論と「圏論をそのまま一階述語論理にのっける公理系」、
・古典論理を採用して置換公理がないのと、直観主義論理で置換公理があるもの
579:１３２人目の素数さん
12/02/07 19:11:10.11
ただの言葉遊び
580:１３２人目の素数さん
12/02/07 22:14:19.35
>>557-568 >>569-576
しょうもない話だな
581:１３２人目の素数さん
12/02/08 02:01:03.73
>>579
プログラムってのは言葉だからな、日常では「言葉遊び」と軽んずるようなことが、
致命的な問題を起こすことがあるのよ。値呼出しと名前呼出しの違いとかな。
もっとも、嘘つきの逆理とかラッセルの逆理とかだって、日常では「言葉遊び」と軽んじられる。
プログラムと違って現実に問題になることもない、本当のお遊びｗ
582:スレタイスレ446
12/02/08 07:44:11.19
>>578
HANDBOOK OF PHILOSOPHICAL LOGICの12巻に大体載ってる。
583:１３２人目の素数さん
12/02/08 13:59:04.85
>HANDBOOK OF PHILOSOPHICAL LOGICの12巻に大体載ってる
どなたか要点だけでも書いていただけないでしょうか？この本がすぐ見えないので
特に、型理論と「圏論をそのまま一階述語論理にのっける公理系」をなぜ考えるのか
ということだけでもいいのですが。
584:490
12/02/08 22:17:01.19
>>534,536
レス遅れてすみません。すばらしい文献を紹介していただいて感謝しております。
夢中で読んでました。勘違いも見つかったり、まあ、とりあえず自分の疑問を治めることが
できました。ただ、ショックなのは、以前ネットをあさって集めた文書の中に、紹介いた
だいた文献が、既にあったことです。なんとも愚かですなあ。
とにかく感謝感激です。ありがとうございました。
585:１３２人目の素数さん
12/02/08 23:39:35.60
>>582
目次見た感じ、圏論っぽい話はないけど、本当にその巻に書いてある？
586:１３２人目の素数さん
12/02/09 01:34:33.86
>>583
Categorical Logicについて勉強したいならばBart Jacobsの大作"Categorical Logic and Type Theory"を読めばいいんじゃないの？
今はペーパバック版が出て安く買えるようになってるはずだし
587:スレタイスレ446
12/02/09 08:00:19.67
>>583
以前こんな書き込みがありました。
623 ：１３２人目の素数さん：2011/11/23(水) 15:34:26.24
＞哲学ではうん十年前から圏論（カテゴリー論）を扱っており、これと数学基礎論を関連付けせず語るのは片手落ちだ。
哲学（論理学？）と圏論の関係って
証明図の代わりにダイアグラムで書こうってもの。
そのために高階直観主義論理⇔トポス
の対応を考えているだけ。
初等トポス⇔ハイティングモデル
選択公理付きトポス⇔ブールモデル
グロタンディークトポス⇔一階無限論理
また逆にトポスを与えたら
Mitchel Benabou Languageという言語がつくれる。
上のような圏論的解釈の完全性定理に該当するものも証明されている。
そして圏論が数学の基礎となるのは初等トポスに自然数、
1→N→N
｜ ｜ ｜
｜ ↓ ↓
└→X→X
を加えて1→0をとったものが集合論に該当しますというだけのことだろう。
588:スレタイスレ446
12/02/09 08:01:45.94
656 ：446：2011/11/26(土) 10:57:45.95
いや、なんでもできるわけではない。
例えばベクトル空間の圏は、cartesian closed にならない。
cartesian closed categoryの上位にmonoidal categoryがある。
cartesian closed は任意オブジェクトA,Bに対して
AｘB→A
↓
B
さらにB^AｘA→Bのユニーク性、また→1をもつもので、
B^AってのはAからBへの射だから、
a→b∧aならばbっていう三段論法が出てくるのすぐわかる、
これでハイティング代数がcartesian closed になることがわかる。
ハイティング代数⇔直観主義論理。選択公理入れれば古典論理完成。
さらにB^AｘA→Bのユニーク性はλ計算の関数適応にも対応。
関数のカリー化からきた考えだから当たり前だけど。
トポスは集合論を解釈する具体的な真偽値を与えるために
subobject classier（これは大抵真と偽の2元集合）を導入したもの。
函手の表現可能性⇔ universal elementの存在なので、
トポスに出てくるΩってのはこれのこと。
例えば集合の圏Setの簡単な例。
2＝{0,1}、Fは函手、集合S'⊆Sのとき、
F(x)＝1(x∊S')
F(x)＝0(￢x∊S')
これがトポスだと以下のようになる...。
S'⇒S
↓ ↓F
1→2(subobject classier)
589:１３２人目の素数さん
12/02/09 21:54:09.74
>>586 >>587 >>588
レスありがとう。今読ませてもらっています。
Jacobsはちょっと高いのでどうしようか．．．
590:１３２人目の素数さん
12/02/10 13:29:32.27
＜コメ作付け制限＞新基準に福島１１市町村が否定的 福島県の１１年産米
緊急調査で放射性セシウムが４月適用予定の新基準値（１キロ当たり１００
ベクレル）を超えた地区があった１２市町村のうち、１１市町村が「１００
ベクレル超５００ベクレル以下」の地区での今春の作付け制限に否定的なこ
とが毎日新聞の取材で分かった。うち４市町は現行の暫定規制値（同５００
ベクレル）を超えた地区でも作付けを認めてほしいとした。農林水産省は自
治体の意向を踏まえた上で２月中にも作付け制限計画をまとめる方針だが、
調整は難航しそうだ。(毎日新聞)
591:１３２人目の素数さん
12/02/10 23:06:31.65
>を加えて1→0をとったものが集合論に該当します
「とった」ってどういう意味だろう？
「公理から取り除く」という意味だとすると、トポスの公理に1→0なんてないし。
「公理として付け加える」という意味だと、1点集合から空集合に射があったら矛盾するし。
同じ言葉が正反対の意味に解釈できるって日本語難しい。
592:スレタイスレ446
12/02/10 23:40:04.42
>>589
圏論的論理学のテキストが無料公開されているのを忘れてました。
URLﾘﾝｸ(www.cs.unibo.it)
ところで以下は型理論学習のための大雑把な予備知識ですが・・・。
λ計算は関数の抽象にλ記号を使った型システムとなります。
型なしλ計算は単一の型を持つシステムとして、やはり型システムに組み込まれます。
究極の型理論として強正規化不能（停止しない式変形がある程度のイメージ、
ただし決定不可能性とは別）ないくつかの型システムがあり、
このシステムの循環する型や、不動点コンビネータを制限することで、
断片としてλ-Cubeと呼ばれる8つの単純型システムからなる構造が得られます。
このCubeのある辺を切り取ると、ゲーデルのDialectica解釈内でのSystem T
（自然数論の無矛盾性証明に導入されました。）が抽出され、
またある辺からはGirardのSystem FやF_ωが抽出され、
CoqやLFなどの自動推論器の原型なども取り出せます。
またCubeのある面は命題論理に、反対側の面は述語論理に対応しています。
こうして取り出された様々な型システムはカリー＝ハワード同型対応によって、
通常の様々な数理論理学の証明規則に各々対応しています。
一方型システムは公理的集合論などの数学の基礎の代替ともなり、
ZFやZFCなどの代わりにQuineのNFやPotterのZU/ZFU、AndrewsのQ_0などが考案されました。
また論理はLTT（通常の論理）とLPT（真偽値を持たない命題を作れる）に分類され、
例えばLPTであるBessonのPT_ω（AczelのFrege構造の形式化）によると、
循環によるパラドクスR∈R<-->~R∈Rの構成さえも許してしまう型システム系の数学が作れます。
593:１３２人目の素数さん
12/02/11 08:58:24.42
>>583
とりあえず>>513の言及している本と>>542のリンク先をそれぞれ見てみたらどうでしょう？
594:557
12/02/11 23:06:33.22
毎度です。>557と関係のあるような関係の無いような話ですが、
CNFに距離空間を突っ込んでHornCNF!=CNFにチャレンジしてみました。
＃数理論理学というよりも計算複雑性の話ですね。
どこか間違っているような気がするのですが、素人なので追いきれず……
どなたかコメント頂けませんでしょうか？
まとめた資料はURLﾘﾝｸ(arxiv.org)にあります。
.tar.gzを付ける必要があるみたいです。
595:１３２人目の素数さん
12/02/12 00:57:16.49
突っ込まなかったけど、>>567について言っておくと、
位相を入れたからって直交は定義できないんですけど。
内積から位相は決まるが、位相から内積は決まらない。
区別は出来ている？
596:557
12/02/12 02:10:25.82
>595
大丈夫です。区別できています。
>567はベクトル空間の間違いですね。
597:１３２人目の素数さん
12/02/12 03:18:53.07
73 ：１３２人目の素数さん：2012/02/09(木) 21:15:32.88
決定性公理 AD って二階算術の命題として定式化出来ますか？
定式化出来るとして、 ADの否定は
ATR0やΠ11-CA0などの体系で証明できますか？
598:１３２人目の素数さん
12/02/12 06:38:58.21
なぜADはATR0やΠ11-CA0などの体系で証明できますか？ではなく
ADの否定は証明できますか、なのだろうか。
599:１３２人目の素数さん
12/02/12 08:34:44.69
選択公理と矛盾する公理じゃなかったっけ
600:１３２人目の素数さん
12/02/12 08:43:40.45
二階算術で定式化できる範囲では選択公理と矛盾しないし（ただし consistency strength は巨大基数レベル）。
つーか、二階算術で定式化できる選択公理もかなり狭い範囲でADと矛盾しないし。
601:１３２人目の素数さん
12/02/12 10:06:01.76
巨大基数レベルってのは巨大基数の帰納的類似物であるような可算順序数レベルってこと？
602:１３２人目の素数さん
12/02/14 10:16:43.45
もちょっと易しい話題にしてくれんかな？
603:490
12/02/15 11:08:49.50
再帰型Tから、T_rectを作るアルゴリズムがご紹介いただいた文献>>534,536 でわかり、
大変感激している最中です。∧、∨、＝や∃までもが再帰型で定義できるというのは
すごい。しかもその定義から作られるT_rectがまさに論理にぴったりとあてはまるのは
不思議としか言いようがない。さて、「再帰型Tから、T_rectを作るアルゴリズム」
というのは、もしかして天下り的に受け取るしかしょうがないのかもしれませんが、
もう少し「再帰型Tから、T_rectを作るアルゴリズム」を深く理解できるような解説
がしてある文献を紹介していただけないでしょうか。あわよくば、「再帰型Tから、
T_rectを作るアルゴリズム」が、当たり前のように思えるようになるといいのですが。
とりあえず今は、圏を知らなければならない気がして予習してます。
どうか偉い方、神様、よろしくお願いします。
604:スレタイスレ446
12/02/15 23:59:02.73
URLﾘﾝｸ(ci.nii.ac.jp)
有名なので既知かもしれませんが
滝田氏の型理論１～４のPDFを参照してください。
Lofの構成的型理論やλ-CubeやL-Cubeの話題まで一通り解説があります。
私はこのPDFで、論理が型理論に埋め込まれる理由が大分理解できました。
※以下、私的メモでレスとは※
URLﾘﾝｸ(www.shayashi.jp)
LET-quantifier condition formula