MSVC /c/Program Files (x86)/Microsoft SDKs/Windows/v7.{0,1}A/Include/ 古いGCC /c/Installed/MinGW/include/ TDM-GCC /c/Installed/TDM-GCC-64/x86_64-w64-mingw32/include/ [追記]gccのパス違った。もっと優先されるパスがある。g++ -v でコンパイルす…

終対象またはモノイド圏の単位対象からの射を「要素」とみなすのは割と自然な発想。デカルト圏なら終対象＝単位対象なので、Cをデカルト圏として、Elt(C) = {e∈Mor(C) | dom(e) = 1 } としてElt(C)を定義する。Elt(C)は単に射の集合で構造を持たない。Cはデ…

豊饒圏をちゃんと定義したい - 檜山正幸のキマイラ飼育記豊饒圏の定義とか、割と詳しく書いている。 関数で関手が表現できるって変でしょ、どういう仕掛けかな？ - 檜山正幸のキマイラ飼育記総称関数が関手の表現に使える事情。 圏論的指数の定義 - 檜山正幸…

結局、自然演繹とはシーケント計算の簡便な別法ってことかと。α = (Γ⇒Δ) が定理シーケント、つまり証明できるシーケントのとき、 Γ ----[α] Δという自然演繹の推論図を使ってイイゾと。また、Γ⇒Δ から Γ'⇒Δ'がシーケント計算で証明できるとき、対応する自然…