次の論文がけっこう参考になりそう。絵が豊富だし、説明も丁寧。 Title:Higher-dimensional categories with finite derivation type Authors: Yves Guiraud, Philippe Malbos URL: http://arxiv.org/pdf/0810.1442v2.pdf Pages: 54p Yves Guiraudってどこか…

モースレベルがシーン（スチル、フレーム）の順序番号を与え、トランジションが隣り合うシーンの移動（move）となる。よって、シーンは証明過程の各段階のスナップショットであり、トランジションは証明ステップとなる。基本トランジションは基本推論、アニ…

定理と証明の関係がよく分からなかったが、そもそもが曖昧だった。ハッキリさせる。定理に関連して3つの概念を導入する。 あるnに対するn-セル（n-ダイアグラム）を命題と呼ぶ。 A, Bを命題として、s:(n + 1) A→B という(n + 1)-セルをステートメントと呼ぶ…

モノイド圏のなかのフロベニウス代数の公理を全部書いてパレットに入れて、フロベニウス代数電卓みたいのは作れそうだ。だいたいはやってみた。現状だと、Workspaceの保存とエクスポートはできるが、リジューム／インポートが動かない、と。これだと、なんと…