条件や性質〈命題〉の定義と、モノの定義は違う。モノを定義するとは、存在させる〈make it exist〉こと。 生成 構成的生成 超越的生成 正当化：存在命題 → スコーレム関数〈選択関数 | セレクター〉 正当化：一意性命題 → 一意値 条件確認〈検証 | 正当化〉

次は同義語 多相型 総称型 型構成子 パラメータ付き型 インデックス付き型 型ファミリー 適切な言葉は型値関数、使うのは型ファミリーにする。型ファミリーとは、Xを集合として、F:X → |C| という写像。Cの対象を型と呼べば、型値関数。X⊆|C| のときが総称型…

ツリーデータ型のモナドのモナドを具体的に書き下すととなると、けっこう難しいようだ。何が障害かというと： 型がうまく定義できない。 空型と単位型 部分集合型、内包的記法 ベキ集合型 直積型 指数型 直和型 依存和型 依存積型 型カインド 処理がうまく書…

フレイド圏の一般化。複数の異なる（異なってもいい）ドクトリンの圏と、そのあいだの関手からなる構造。

わだち圏〈トラック圏 | track category〉は、今風に言えば (2, 1)-圏。 k ＞ 2 なk-射は自明 k ＞ 1 なk-射は可逆 ホム圏は亜群になるので、亜郡豊饒な圏。特別な例として： ホムセットが亜集合である圏＝ホムセットに同値関係が載っている圏 わだち圏をベ…

丸山先生の記事で、「アブラムスキー・クッカ対応」と書いてあったけど、「クッカ」に近いのか。それと、この対応はもっと昔の人の名前を使って「カリー・ハワード・ランベック対応」がより一般的だと思う。圏論と量子情報・計算を対応づけたのはアブラムス…

コンピューターサイエンスの学習は、職業エンジニアになることを阻害する https://zenn.dev/nakanishi/articles/d3d8ff5529832f2acf6c 言っていることは正しいし、こういう意見の人はけっこう多いけど、まとまった文章がないから助かる。記事を消してしまう…

＠2020-09-30 20：00--22:00 by Zoom vs にならなかった。 谷村先生の絵が力作。 パットナムの双子地球が批判されていた。 双子地球の“水”は、心的状態が一致しても外延が一致してない例らしい。 SF、ファンタジーとしては面白い気がするが、フィクションと…