自然演繹系のUIをglobular風にする。 globular 自然演繹系 パレット パレット セル 項（ターム） ラベル ラベル（名前） 色 (なし) 次元 次元 ダイアグラム 式 キャンバス ノート キャンバスビュー ノートエリア コマンド コマンド コマンド Globularのコマ…

Γ#30Φ の構成法： ΓをSelectする。 ビューを(Γ:3)(project=1, Slice=0)にする。ナリティ1の射影で、スライスに β:2 f->g:1 A->B が見える。この状態なら、ビュー上で次元差1となり j:1:B->C をアタッチ可能。 j:1:B->C をアタッチする。結果的に、Γ[B]j とい…

参考： http://pages.vassar.edu/mccleary/files/2011/04/FinalChapter9.pdf http://pages.vassar.edu/mccleary/files/2011/04/FinalChapter10.pdf grating（格子張り）はtilingと同じ意味。gratingは次元によらずに使える言葉かもしれない。tilingは2次元ぽ…

n-圏のn-射は、n-ペースティング図またはn-ストリング図で幾何実現される。ペースティング図もストリング図もダイアグラムと呼ぶ。ダイアグラム（ペースティング図でもストリング図でも）の幾何実現は素片化空間（stratified space）である。 圏 ペースティ…

球体状n-圏（globular n-category）において、次元が違う射を、恒等引き上げ（identity pull up）を使ってから結合することをヒゲ操作（whiskering; ウィスカリング）と呼ぶ。このとき、射の次元の差を次元差と呼ぶ。ヒゲ操作は、射を表現するダイアグラムに…

公開ワークスペースの数は、作者の jamievicary@gmail.com が圧倒的に多いが、その他の人、2015-12と2016-01にpublishした人： 2015-12-04 cdouglas@mit.edu 2015-12-07 schommerpries.chris@gmail.com 2015-12-07 casparwylie@gmail.com 2015-12-08 dominic…

射の形状（shape）名前をXとする。Xの事例は： 単体（simplex） 球体（globe） 方体（cube） オペトープ（opetope） マルチトープ（multitope） デンドレックス（dendrex） テータ・セル（theta cell） それぞれの形状の説明はだいたいnLabにある。 https://…

IDEの意味で「プロジェクト」を使っていることがある。例：画面下部にあるProject Abstract。しかし、Projectはビューコントロールにもあるし、通常は射影操作や射影のナリティ指定に使う。 射影のナリティをProjectコントロールで指定するが、論文・マニュ…

ストラータムは素にはならない。ストラータムはさらに分割されるのだ。ストリング図のワイヤーが、ストリンググラフのエッジと境界頂点、内部頂点に分割されるように、ストラータムも分割される。

やはり次元概念が難しい。以前、幾何次元、グレード次元という言葉を使ったが、これはやめよう。射の次元を次数（degree）として、幾何次元を次元としている例がある。 セルは指標＝コンピュータッドの要素の意味で使う。幾何胞体とは異なる。幾何胞体は単純…

動詞squashiはペチャンコに潰すこと。ストリング図のキャンバスボックスを低次元のボックスに射影するとき、重なっているストラータムを低次元に押し込むときにスカッシングをする。スカッシングは、ファイバー方向に並んだストラータムを評価する。つまり、…

射、セル、ストラータムなどの次元を区別するために、 "Surface diagrams for gray-categories" by Hummon, Benjamin Taylor（ http://escholarship.org/uc/item/5b24s9cc, http://www.chimaira.org/archive/SufraceDiagramsForGrayCategories_eScholarship-…

タイリングの矩形タイルをブリック（レンガ）とかブロックとか呼ぶこともある。レゴブロックとか、ドミノ牌（牌はタイルの意味）とも言える。ブリック・コンストラクション・ゲームという言葉もあったな、そういえば。牌、タイル、ブリック、ブロックにはラ…

ダイアグラムはキャンバス空間内の模様だが、 キャンバス空間＝キャンバス矩形＝キャンバスボックス＝ボックス エクステント＝一般化ストリング＝ストラータム（stratum; 層素） 0-ストラータム＝ノード＝ドット＝点＝頂点 1-ストラータム＝シーム（縫い目）…

Globularのセルは、セル複体（胞複体）のセルとは全然違う。コンピュータッド理論の生成射（generating morphism）なのだと思う。高次圏の高次射をセルと言うが、これとも違う。任意の高次射がセル（生成高次射）なわけではない。n-セルとn-ダイアグラムの帰…

ソフトウェア： http://globular.science/ ヘルプ： https://ncatlab.org/nlab/show/Globular 論文 Title: Globular: an online proof assistant for higher-dimensional rewriting Authors: Krzysztof Bar, Aleks Kissinger, Jamie Vicary Pages: 18p URL: …

Saveはサーバー側に保存するので、アカウントが必要。 Export, Importはローカルストレージとメモリーのあいだのやり取りなのでアカウント不要。 ワークスペース名.jsonでエクスポートされる。 インポートはローカルから読む、かなり速い。 Graphicはimage.p…

コンピュータッドとか雑多に色々考えてみる、ほんと雑多 - 檜山正幸のキマイラ飼育記 メモ編で類似性という概念に触れた。次のことが言えると思う。 すべての命題は類似性の主張である。 すべてのメタ命題は存在命題である。 すべての証明は構成的である。 …

コンピュータッドは、言い換えれば多グラフだが、「形容詞「複」「多」と箙〈えびら〉 - 檜山正幸のキマイラ飼育記」に従えば、高次多箙（higher polyquiver）のことだ。1-quiver＝普通の有向グラフのときと同じに、生成形から自由生成できる。高次多箙の生…

キャンバス空間は図を描く（レンダーする）場所。図形の埋め込み先としてはアンビエント空間と言ったほうがいいかもしれないが、描画だからキャンバスにしておく。n次元キャンバス空間に絵図が描かれているとして、幾何次元nのセル（チャンバー）はグレード…

Isabelleの用語法の無茶苦茶さや、概念の混乱、理解のためのミッシングリンク、これらの大きな部分は「次元概念の欠如」によるのではないだろうか？ -- まず間違いない。 参考：シーケント計算、ムービー、高次圏 - 檜山正幸のキマイラ飼育記 メモ編 参考：…

名前 Globular Quantomatic FQL IDE 形態 Webアプリケーション デスクトップ デスクトップ 実装言語 JavaScript ML + Scala Java 記述言語 なし なし 4種類あり エンジン分離 不可 可能 不可 データ交換 バイナリ JSON ソースコード 背景理論 グレイ圏 対称…

Globularとの関係は、Quantum Groupが作った以外は無関係だけどね。ホームページ（サイト） https://quantomatic.github.io/ ダウンロードボタンを押すとすぐさまダウンロードになるので注意。ダウンロードファイルは、QuantoDrive-＜プラットフォーム＞-＜…

球体モデル その双対 k-球体セル (n-k)-エクステント 始端 後域 終端 前域 0-セル n-エクステント n-セル 0-エクステント 球体複体 領域分割図 共端（平行） 共域 境界で隣接 間域で対面 セルの回りの扇 エクステントの境界 ブリッジセルで疎通 境界エクステ…

絵素： お絵描きの基本素材 絵図的操作： 絵素の組み合わせ方や絵素の変形加工法、構成的・作業的 部品： 与えられた基本の絵素から絵図的な操作で作ったモノ。後で使うためにストックする。 神託： 絵図的な操作で作れないものを作ってくれる神様がいるので…

次のあたりでかなり記法法を工夫して整合的に仕上げている。 非対称閉圏のカリー化：記号法を工夫すれば、右と左の混乱も解消 - 檜山正幸のキマイラ飼育記 自画自賛：右と左が気持ちよくなった件 - 檜山正幸のキマイラ飼育記 コンパクト閉圏と絵算で理解する…

Globularで古典テンソル計算 - 檜山正幸のキマイラ飼育記 メモ編 : 冗談ではないよ、マジ、マジ。絵算の起源（のひとつ）は、ペンローズがテンソル計算の代替に使っていたペンローズ・ヒエログリフなのだから、古典テンソル計算が絵算で出来るのは当然なのだ…

冗談ではないよ、マジ、マジ。絵算の起源（のひとつ）は、ペンローズがテンソル計算の代替に使っていたペンローズ・ヒエログリフなのだから、古典テンソル計算が絵算で出来るのは当然なのだ。絵算の電卓ソフトとしてGlobularを使う。問題点は、Globularがラ…

バートレット（bartlett）についてはけっこう書いている。表記がアルファベットとカタカナと統一されてないんだけど： http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=bartlett http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=%A5%D0%A1%BC%…

ワークスペース管理：これは深刻、せめてセーブ時刻を表示してほしい。 パレット内のサムネイルの順序の並べ替え。これも深刻。 パレットの内容をテキストとしてダンプ 今見てるセルのsourceやtargetを取りたい。Resrictだけでは取れないことがある。 穴あき…