[追記]事情が分かりました。最後に書き足してます。[/追記]
一昨日紹介したGlobularの使い方を説明するために、簡単な例題とかを作ってます。
Globularにはソースコードとかデータという概念がなく、ソフトウェアの状態(ワークスペース)のセーブとリストアができるだけです。僕の環境だと、セーブはできるのだけど、うまくロードできない。他の人が作ったワークスペースはロードできるので、僕固有の問題かも知れません。
次のようにして僕のサンプルをロードできる(またはロードできない)ので、どなたか試してくださいませんか。
- http://globular.science/ をChromeで開く。
- 画面上部のメニューから[GALLERY]ボタンを押す。
- ギャラリー番号の1601を選ぶ。
- Author: hiyama@chimaira.org の exercise: commutative monoid を選ぶ。
次のURLにダイレクトにアクセスしても同じはずです。
[追記]
日本語(非ASCII)の文字が入るとダメなようです。ASCIIだけで書き直しました。
GUIからの手順は、最後のところで v2, v3(Version 2, 3)を選んで下さい。これの中身は、対称モノイド圏のなかのひとつの可換モノイドを書き下したものです。v2は公理のみ、v3は定理をひとつだけ証明しています。
[/追記]