rw h は等式的法則 h （hは等式的法則のラベル）を使ってターゲット内の項を別な項で置き換える。 rw ←h とすると、a=>b 方向のリライトをする。矢印が逆！ rw h とすると、a まったく！

constantは、域が単位対象＝空リストである射を宣言する。図では三角ノードになる。variableは、名前付きのワイヤーを準備する。意図としては、その名前付きワイヤーはラムダ束縛するつもりだから、事実上束縛変数の選言。変数名は混乱の原因になるから、で…

https://leanprover.github.io/reference/tactics.html#basic-tactics This tactic applies to a goal whose goal has the form t ~ u where ~ is a reflexive relation, この言い回しにはさんざん悩まされた。「ゴール」に意味が。 証明状態 メインゴール …

デカルト閉復圏とラムダ計算 - (新) 檜山正幸のキマイラ飼育記 メモ編、ラムダ図 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。とても良い描画法を思いついた。青で書いているのは黒がなかったせい。ラムダハウスは関手ボックス／関手ストライプ／オペレ…