圏の下部構造は有向グラフです。圏には恒等射がありますが、恒等射に相当する特別な辺を備えた有向グラフは反射的有向グラフと呼びます。よって、圏の下部構造は反射的有向グラフだと言ってもいいでしょう。圏を一般化した構造である一般化圏〈generalized c…

「論理や型理論の圏論的意味論」より： 今年いっぱいくらい、まとまった時間が取りにくい状況があるので、長いブログエントリーは書けそうにない。短いエントリーをチョコチョコと書くことにします。短くて完結した書き物は難しいので、続き物になる可能性が…

ひとつ前の記事「圏論のエンドとコエンドは双対なんだよ」において、“連立方程式系の解空間”と“関係族の同値閉包による商集合”が双対的だという話をしました。この双対性はちょっと不思議な感じがします。最終的には、写像（集合圏の射）の並行ペア（両端が…

エンドとコエンドは、その名前から双対なんだろうとは誰でも思うでしょう。しかし、定義の仕方によっては双対性が見えにくいこともあります。この記事では、エンドとコエンドの双対性が出来るだけ見えやすくなるような定義と記法を提示します。$`\newcommand…

複圏〈オペラッド〉はその下部構造に複グラフを持ちます。導出システム〈演繹系〉は、概念的には複グラフそのものです。複グラフを依存型理論で利用したいとき、複グラフにも依存性を導入する必要があります。この記事で、依存性を持つ複グラフを導入します…

「論理や型理論の圏論的意味論 // 導出システムの圏と圏の圏」において、導出システム達を対象とする圏に触れました。しかし、導出システムのあいだの準同型射（それが圏の射となる）を素朴に考えていては、どうもうまくないようです。導出システムは、複圏…

例えば、有向グラフやラベル付き有向グラフの説明をするとき、当然に記号的表現を使うわけです、 $`\mathrm{Graph}(A, B)`$ とか。ふと、使っている記号的表現 $`\mathrm{Graph}(A, B)`$ を文脈から切り離して眺めてみました。「文脈無しで、$`\mathrm{Graph…

今年いっぱいくらい、まとまった時間が取りにくい状況があるので、長いブログエントリーは書けそうにない。短いエントリーをチョコチョコと書くことにします。短くて完結した書き物は難しいので、続き物になる可能性が高いです。$`\newcommand{\mrm}[1]{ \ma…

過去記事「矢印記号の使用法と読み方 2024」において、様々な矢印記号の意味・運用について述べました。構文論で使う矢印記号に関して、別な読み方・名前を追加して一覧表を再掲します。 矢印記号 読み方 別な読み方・名前 $`\Rightarrow`$ 含意〈implies〉 …

記号的表現を見たとき、十分トレーニングされた人は、周囲の文脈から様々な“忖度”をして、記号的表現を解釈します。「行間を読む」と言ってもいいでしょう。ソフトウェアによって「忖度する／行間を読む」行為を実装することはとても大変です。ソフトウェア…

随伴系〈adjunction〉の典型的例というと、やはり自由忘却随伴系〈free-forgetful adjunction〉でしょうかね。あと、カリー化・反カリー化も典型的だと言えるでしょう。集合圏で考えるとして、カリー化・反カリー化による次のホムセット同型があります。$`\n…

ひとつ前の記事「球体集合と組み合わせ幾何」で、球体集合の圏についておおよそは説明しました。この記事では、次元が低い球体集合達の圏について述べます。球体集合の絵図表示であるペースティング図とテキスト表示である指標についても補足します。低次元…