- 109 名前：ご冗談でしょう？名無しさん mailto:sage [2013/08/04(日) NY:AN:NY.AN ID:???]
- >>76
researchmap.jp/mu1x9nhhd-21099/?action=multidatabase_action_main_filedownload&download_flag=1&upload_id=40760&metadata_id=12105
> 定義 2.13 型理論の言語 L^T は以下の要素を持つ
・・・
> * 任意の項τに対し、ある n が存在して項σが type n であり、項τが type n+1 を持つ時
> のみ論理式 σ∈τ は有意味な論理式となる。
x∪{x} = {y | y∈x or y∈{x}}
変数ｙのtypeは何になるかね？
