図式をユーザインタフェイスとした圏論のための証明支援システムの設計を行 う。システムの内部では、形式的証明に論理式を用い、ユーザへの表示には図 --1 のような図式を用いる。証明支援系は命題の入力と証明の実 行という二つの機能を持つが、我々はその両方とも図式上の操作として実現し ようと考えた。つまり、命題の入力は図式の作成によって行う。このためのコ マンドを描画コマンドと呼ぶ。証明の実行は図式上でのマウスのクリック等に よって行う。このためのコマンドを証明コマンドと呼ぶ。特に証明コマンドの 一つである「貼り付け」コマンドは、視覚的にわかりやすく証明を表している。