バエズの留め金（クラスプ）を使って、ベータ変換とエータ（イータ）変換の絵を書いた。恒等射のラムダ抽象のベータ変換は随伴の余単位、エータ変換が随伴の単位を与える。バエズの留め金を使うと、ニョロニョロ関係式が比較的自然に描ける。後日、スキャン…

Cが非対称（対称とは限らないという意味）厳密モノイド圏だとして、対応する多圏Poly(C)を定義する。S = |C|*（クリーネスター）として、Sは連接で厳密なモノイドになるとする。α = (A1, ..., An), β = (B1, ..., Bm) をSの要素として、PolyHom(α→β) := C(<α…

「本棚 右の壁から10面目、11面目」のなかに、なんか変な論理本。 「本棚 右の壁から6面目、7面目」のなかに『論理学をつくる』 「本棚 右の壁から4面目」にも変な論理本。隣の本がタイトル見えないが、なんだ？ 「本棚 右の壁から4面目」のなかに『ゲーデル…

セルの次元は描画時にbump upしているので、描画キャンバス次元は1次元上がっている。 高次圏 シーケント ムービー 0-セル 命題 絵の一部（ワイヤー） 1-セル シーケント スチル 2-セル 推論、証明 トランジション、ムービー 3-セル 証明の変形 ムービームー…

竹内／八杉のあの『証明論』が見つからない。カット消去がちゃんと載っているのはアレくらいだろう。

20070416 直積と射影がらみの高階関数たちの相関図 - 檜山正幸のキマイラ飼育記 20090325 演繹系とお絵描き圏論 - 檜山正幸のキマイラ飼育記 今、けっこう真面目に考えている。多圏の導入と使い方。[追記]だいたい出来た→ http://d.hatena.ne.jp/m-hiyama-me…

「ならば」記号があると、左右または上下がある。その部分は何と呼ぶのだろう。まったく確信がないが、 A⊃B で、Aが前件（antecedent）でBが後件（consequent）だったか？ 前件／後件は条件法（conditional; 条件表現、条件文）に対して使われる言葉だと思う…

⊃ implies |- provable（probableじゃない、注意） ⇒（シーケント） entailsかな |= valid, satisfies A |- B に対して、B is provable from A のようになる。|= A も A is valid。A |- B を A proves B と読むとおかしいのかな？ proveする主語はAじゃなく…