ひとつ前の記事「Propositions-As-Typesを曲解しないで理解するために」の最初の節や最後の節で、同義語・曖昧多義語を話題にしました。曖昧さは色々な形で現れます。なにごとかを正確に理解するには、曖昧さを処理していくことが必要です。まー、曖昧に書く…
「贅沢なグロタンディーク宇宙とPropositions-As-Types」に対して、老婆心的な補足をします。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } \newcommand{\In}{\text{ in }} `$内容： 「命題」を排除したい！ ベリティ型とその型…
次の2つの記事の続きです。 贅沢主義者のグロタンディーク宇宙 型・インスタンス・宇宙とタルスキ宇宙系列 Propositions-As-Typesというよく知られたキャッチフレーズを、グロタンディーク宇宙の観点からなるべく明確にします。$`\newcommand{\mrm}[1]{\math…
「贅沢主義者のグロタンディーク宇宙」でグロタンディーク宇宙の話をしました。贅沢主義か節約主義かは、公理系を設定するときの態度であって、どちらの態度で公理系を設定しても、得られる概念は同じです。ところで、単一のグロタンディーク宇宙ではなくて…
たいていの公理系はミニマリスト・アプローチで定義されていて、無駄な（他の公理達から導出可能な）公理は入れないで、必要最小限の公理達から構成されています。しかし、導出可能な命題を最初から公理系に入れておくのが絶対にダメなわけではないです。「…
ダラッっと語る。$`\newcommand{\In}{\text{ in }} \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } %\newcommand{\u}[1]{\underline{#1} } %\newcommand{\Imp}{\Rightarrow} %\newcommand{\If…
同一の概念にたくさんの呼び名があるのは、よくあることです。呼び名が違うことで同一性に気付かなかったり混乱したりします。表題にある概念の同一性について整理しておきます。$`\newcommand{\In}{\text{ in }} \newcommand{\mrm}[1]{\mathrm{#1} } \newco…
「スライス圏の大域的な定義： スラッシュ記号の解釈」で、スラッシュ記号 '$`/`$' で表現されるスライス構成について述べました。そこで次のように書きました。 二番目の $`f^*`$ は定義に条件が必要で複雑でもあるので、ここでは一番目だけを扱います。 過…
以下の過去記事達で指摘した問題の一部に対する対策をします。 型理論に出てくる第一射影と第二射影 最近の型理論のハマリ所 ファイバー積の場合の第一射影と第二射影で使う記法を新たに約束します。双対であるコファイバー和についても論じます。$`\newcomm…
木〈ツリー〉や林〈フォレスト〉は重要なデータ構造です。以下の過去記事で説明したことがあります。 木と林（有向グラフ） 木と林（有向グラフ） その2 レベル付き林の圏 （最後の追記参照） カートメル〈John Cartmell〉による木・林の定義が使いやすいと…
「論理計算のための宇宙と型、二種類の述語」において、二元の宇宙 $`{\bf Prop}`$ を次のように定義しました。$`\quad {\bf Prop} := |{\bf Bool}|`$$`{\bf Bool}`$ は2つの対象 $`{\bf 0}, {\bf 1}`$ だけを持つ集合圏の充満部分圏です。しかし実際の証明…
[追記]「論理計算のための宇宙と型 補遺」に続きがあります。[/追記]型理論と圏論の言葉は次のように対応します。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mfk}[1]{ \mathfrak{#1} } \newcommand{\In}{ \text{ in } }`$ 型理論 圏論 型 対象 型…
一部の証明支援系／プログラミング言語において、シグマ型を直積型と同じ '$`\times`$' で、パイ型を指数型と同じ '$`\to`$' で書くという記法が採用されています。これは短く書けて便利なのですが、当然ながら混乱を招くので、少し変更した形で紹介します。…
色々とハマル。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\In}{\text{ in }} \newcommand{\op}{ \mathrm{op} } % used \newcommand{\hyp}{\text{－} } % used \newcommand{\ILT}{ \triangleleft } % immediately…
以前、圏論の普遍性という概念は難しい、という話を書いたことがあります。 圏論の普遍性が難しい理由 普遍性は“前層の表現可能性”により語られるので、普遍性の難しさは“前層の表現可能性”の難しさです。「表現可能である」ことは前層の性質ですが、「当該…
日記風にダラッと書きます。ヴォエヴォドスキー〈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〉を採用しました…
インスティチューション理論の骨組みに、型理論やモナドを使って肉付けしようという目論見（「構文付き変換手インスティチューション 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〉の包括圏…
「球体集合達の圏の構文表示 1/2」の続きです。この機会に、型理論的な形式的体系と構文的データについて詳しく説明します。一方、形式的体系の構文圏と圏同値の話は、概要を急ぎ足で述べるだけになってしまいました -- いずれ補足する機会もあるでしょう。$…
