このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

雑記/備忘

GAT〈ガット〉

日記風にダラッと書きます。ヴォエヴォドスキー〈Vladimir Voevodsky〉のC-システム(「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照)は、名前を変更しただけでカートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉と…

型理論的形式体系の構文代数系はファイバー付き依存多圏

型理論的形式体系〈type-theoretic formal system〉とは、抽象的演繹系(「演繹系とオペラッド」参照)の一種で、基本的な構文構成素としてコンテキストと何種類かの判断を持ちます。型理論的形式体系があると、コンテキストを対象として、コンテキストのあ…

複前層の圏とファミリー付き圏

「ヴォエヴォドスキーの宇宙圏とパルムグレンの複前層」で述べたように、ヴォエヴォドスキーとパルムグレンは、同じ時期に同じ概念を独立に考えていたようです。その概念を、パルムグレンによる呼び名 "multivariable presheaf over $`\mathcal{C}`$" を縮め…

型理論に出てくる第一射影と第二射影

ファミリー付き圏〈category with families | CwF〉やC-システム〈C-system〉(コンテキスト圏〈contextual category〉と同じ)など、型理論の構文的側面を圏論的に定式化した圏(型理論的圏)では、「射影〈projection〉」と呼ばれる射が登場します。射影が…

ヴォエヴォドスキーの宇宙圏とパルムグレンの複前層

最近、カートメル/ヴォエヴォドスキーのC-システム(「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照)に興味を持っています。で、次の論文を眺めてみました。 [Voe14-15] Title: A C-system defined by a universe category Author: Vl…

パチモンの圏 = システム

「C-システム、分裂ディスプレイクラス、カートメルツリー」より: ヴォエヴォドスキー〈Vladimir Voevodsky〉は、型理論の理論〈theory of type theories〉の基礎としてカートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉を採用しました…

C-システム、分裂ディスプレイクラス、カートメルツリー構造

インスティチューション理論の骨組みに、型理論やモナドを使って肉付けしようという目論見(「構文付き変換手インスティチューション 1/n」における“半具象インスティチューション”)は、型理論的圏の反対圏が指標の圏として使えることが分かってちょっと進…

型理論とインスティチューション理論が繋がるぞ!

ビンゴ! 「インスティチューションの“指標の圏”の具体化として、型理論的圏の反対圏をとればいいだろう」と見当をつけていたのですが、アタリだったようです。型理論的圏は、拡張包括構造を持ちます。拡張包括構造を持つ圏上の、プルバック四角形(コスパン…

ファイブレーションの亀裂と分裂

昨日の記事「拡張包括構造のもうひとつの定式化」で次のように書きました。 $`\mathrm{Disp}`$ が関手になるとき、選択した $`(d, f) \mapsto f^\# d`$ 達を、ディスプレイクラス $`\mathscr{D}`$ の分裂子〈splitting〉と呼びます。分裂子を持つディスプレ…

拡張包括構造のもうひとつの定式化

拡張包括構造については、「最近の型理論: 拡張包括構造を持ったインデックス付き圏」で述べたことがあります。型理論的圏(「指標の圏はコンテキストの圏の反対圏」参照)は、なんらかの拡張包括構造を持ちます。拡張包括構造の定式化は色々とあります。ジ…

パルムグレンによる、型理論の複前層モデル

パルムグレン〈Erik Palmgren〉は、圏の“前層の圏”を作る操作を繰り返し適用することにより、依存型理論の圏論的モデルを構成しました。パルムグレンのモデルは、カートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉の“印象的な具体例”を与…

型理論とインスティチューションの周辺

紹介している資料は、「依存型理論の圏論的セマンティクスの資料」と一部重複しています。$`\newcommand{\cat}[1]{\mathcal{#1}}`$ 構文論と形式言語 構文モナド 相対モナド 構文論と形式言語インスティチューションは、構文論と意味論の枠組みを与えます。…

指標の圏はコンテキストの圏の反対圏

「構文付き変換手インスティチューション 1/n」において、半具象インスティチューション〈semi-concrete institution〉という言葉を出しました。インスティチューション理論における指標の圏〈category of signatures〉やモデル関手〈model functor〉は、公…

集合のバンドルと圏のバンドル

集合のバンドルは便利に使えます。集合のバンドルの圏化〈categorification〉はファイバー付き圏〈fibered category〉がふさわしいでしょうが、もっと素朴な“圏のバンドル”も定義しておいたほうが良さそうです。例えば、ジェイコブス〈Bart Jacobs〉の包括圏…

球体集合達の圏の構文表示 2/2

「球体集合達の圏の構文表示 1/2」の続きです。この機会に、型理論的な形式的体系と構文的データについて詳しく説明します。一方、形式的体系の構文圏と圏同値の話は、概要を急ぎ足で述べるだけになってしまいました -- いずれ補足する機会もあるでしょう。$…

球体集合達の圏の構文表示 1/2

「指標の話: 形状の記述と形状付き集合」において、形状付き集合について述べました。よく使われる形状付き集合に球体集合〈球体的集合〉があります。球体集合達の圏の部分圏(有限な球体集合達)に対して、その構文表示を考えましょう。圏の構文表示とは、…

矢印記号の使用法と読み方 2024

矢印記号の使い方が、分野やコミュニティごとにバランバランで困ったー、という話題は、大昔から何度も繰り返しています。 さまざまな「ならば」達 (2006年) 論理記号のいろいろ (2006年) 論理:証明可能性と普遍妥当性 (2009年) 型推論に関わる論理の概念と…

再帰的構成のために: 順序数の圏

この記事も実はマルカキス論文(「指標の組織化と表現方法と呼び名は色々だ」参照)に触発された指標/コンピュータッドに関わるネタなのですが、独立な話として読めるので、タイトルに「指標の話:」とは入れてません。順序数に沿って再帰的構成や帰納的証…

指標の話: ペースティング図とバタニン・ツリー

高次圏の射達の組み合わせを表現する方法のひとつとして、ペースティング図があります。ペースティング図は、テキスト形式に書き写すことができます。ペースティング図とテキスト形式の中間の形式として、バタニン・ツリーがあります。バタニン・ツリーはと…

指標の話: 形状の記述と形状付き集合

昨日の記事「指標の組織化と表現方法と呼び名は色々だ」において、イワニス・マルカキス〈Ioannis Markakis〉の論文 "Computads for generalised signatures" を引き合いに出しました。このマルカキス論文には、色々なことが書いてあって面白い。面白いトピ…

指標の組織化と表現方法と呼び名は色々だ

以下の論文、タイトルを見て興味をそそられました。が、「んっ? 思ってたのと違う」となりました。コンピュータッドも指標も僕が知っているコンピュータッド/指標とは定義が異なるのです。が、冷静になって考えると「あっ、やっぱり同じか」となりました。…

フレーム充填問題と解空間関手

フレーム充填問題(「圏論におけるフレーム充填問題」参照)の解の全体、つまり解空間は、ファイバー付き圏のバンドルになります。フレーム充填問題のフレーム付き指標は、フレーム条件にファイバー付き圏のバンドルを対応させる関手を定義します。このこと…

モノイドの片側逆元

一般的に、モノイドの要素が右逆元を持っても左逆元を持つとは限りません。これは正しいのですが、ある特定のモノイドをとったときには、右逆元の存在が左逆元の存在を導くことはあります。n次正方行列の掛け算のモノイドは、「右逆元の存在から左逆元の存在…

射のクラスと制約付きスパン 補遺

「射のクラスと制約付きスパン」に出した具体例に対して、「あれ、この例はダメかも」と取り消して、すぐ「ん? 大丈夫だわ」ともとに戻しました。この補遺記事で、事情・経緯を書いておきます。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}[1]…

射のクラスと制約付きスパン

圏のスパンの全体は、プルバックを使って圏にすることができます。スパンの左脚と右脚に制約を付けても圏を構成できるときがあります。こうして作った制約付きスパンの圏が役に立つことがあります。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}…

続・変換手意味論とブラケット記法

この記事は、「変換手意味論とブラケット記法」の続きです。追記にするには長すぎるので別記事としました。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}[1]{ \mathcal{#1} } %\newcommand{\op}{ \mathrm{op} } \newcommand{\In}{\text{ in }} \…

変換手意味論とブラケット記法

変換手意味論が何であるかを説明し、変換手空間の便利な略記法であるブラケット記法を紹介します。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}[1]{ \mathcal{#1} } %\newcommand{\op}{ \mathrm{op} } \newcommand{\In}{\text{ in }} \newcomma…

等式的2-グラフ(2-圏の記述のために)

等式的2-グラフ〈等式的2-コンピュータッド〉について解説します。等式的2-グラフは、2-圏内で実現される構造を記述するための具象指標として使います。例えば、2-圏内の随伴系やモナドは等式的2-グラフで記述できます。$`\newcommand{\mrm}[1]{ \mathrm{#1}…

圏の具象性に関する資料

検索でたまたま引っかかった次の論文をチラ見しました。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\T}[1]{ \text{#1} } `$ [Pag11-] Title: Concrete Fibrations Author: Ruggero Pagnan Submitted: 24 May …

グロタンディーク構成・逆構成と同値対応

グロタンディーク構成には逆向きの構成があって、それらのペアが“インデックス付き圏の圏”と“ファイバー付き圏の圏”の圏同値を与えます。バンドル-ファミリー対応はその特殊ケースです。前層と“要素の圏”の対応も特殊ケースとなります。そのへんの事情をこの…