なんかのバグで水平線が表示されたり、されなかったり。ドットが水平線の場所。ブラウザにも依存するようだ。なんだよコレ 型構成＝対象構成 依存型理論： 対応する圏論： 関数データ構成＝ポイント射構成 依存型理論： 対応する圏論：

Leanの論理再考 - (新) 檜山正幸のキマイラ飼育記 メモ編 まだ続く。 x:X |- P(x) :Type ------------------- パイ型形成子 Πx∈X.P(x) :Type x:X |- f(x):P(x) ------------------- 依存ラムダ抽象 Λx:X.f(x) : Πx:X.P(x) x:X |- A :Type ------------------…

全称限量子とタプル - (新) 檜山正幸のキマイラ飼育記 メモ編： もっと考えないと。 最初に、 連言ボックス、選言ボックス、全称ボックス、存在ボックス - (新) 檜山正幸のキマイラ飼育記 メモ編 と 選言ボックスと二面ノード - (新) 檜山正幸のキマイラ飼育…