「型理論周辺、何で混乱するのか？」において： 型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです 地雷原になってしまう大きな理由に、ターンスタイル記号 '$\vdash$'、二重矢印 '$`\R…

どこに引っ越すのか？ それは“コンテキスタッドの世界”への引っ越しです。コンテキスタッドが型理論／論理／インスティチューション理論に対して、統合的・整合的な枠組みを与えるだろう、と思っています。それは、最近の記事達の内容や動機になっています。…

型理論周辺の用語・記法・説明が混乱誘発的〈confusing〉で、それは僕の長年の悩みの種です。型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです*1。最近、包括コンテキスタッド（「型理論…

包括圏とコンテキスタッドの組み合わせは、型理論やインスティチューション理論に向いているようです（「型理論とコンテキスタッド： コンテキストフル射」参照）。この記事では、包括コンテキスタッド（包括圏とコンテキスタッドの組み合わせ）を定義し利用…

集合 $X$ 上の方程式が与えられたとき、その解集合（空集合でも $X$ 全体でも、なんであれ）は一意に決まると我々は信じています。しかし、トポスのなかで方程式を考えると、解集合（に相当する解対象）は一意に決まることは保証されません。これって、…

圏の恒等射だけで部分圏ができます。が、この部分圏はファイブレーションクラスにはなりません。包含的圏（「色々な包含的圏」参照）の包含射達は部分圏を形成しますが、これもファイブレーションクラスにはなりません。圏のファイブレーションクラスの定義…

「名前の解釈： 正確なコミュニケーションのために」、「名前の解釈 その2」の続きです。$`\newcommand{\In}{\text{ in }} \newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] } \newcommand{\hyp}{ \text{－} } \newcommand{\mbf}[1]{ \mathbf{#1}…

「名前の解釈： 正確なコミュニケーションのために」の続きです。$`\newcommand{\In}{\text{ in }} \newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] } \newcommand{\hyp}{ \text{－} } \newcommand{\mbf}[1]{ \mathbf{#1} } \newcommand{\mrm}[1…

名前の解釈をちゃんとしよう -- と、口頭では何百回も言った気がするのですが、ちゃんと書いたことはなかったので、この記事にまとめておきます。名前を正確に解釈せずにボヤッとした印象で済ませてしまう癖を矯正するのは難しいですね。それが、何百回も言…

カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉のコンテキスタッド（「コンテキスタッド、包括圏、ハイパードクトリン」参照）は、型理論と思いのほか相性がいいようです。ちょっと驚いています。型理論的概念である包括圏を、テレスコープ構成によ…

「色々な包含的圏」において、包含的圏の変種を6種類定義しました。圏の対象達全体の集合に載る大域的な構造と、各対象ごとに構成できる局所的な構造の2つの観点から分類しています。この記事では、包含的圏（の変種）の事例であり、同時に誤解しやすい点に…

包含的圏〈inclusive category〉の定義は人により色々です。型理論やインスティチューション理論に使うことを目的にして、包含的圏に関して整理しておきます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]…

「導出系： 反省と課題 // ソート付き集合の圏は変わる」において、ソート付き集合達の圏 $\mathbf{SortedSet}$ を導入したのですが、その定義は関係をベースにしています。関係をベースにした定義は、どうも分かりにくいし扱いにくいので、ファミリー〈集…

カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉のコンテキスタッドは、最近の記事「コンテキスタッドかぁ、ウーム‥‥」で紹介しました。依存アクテゴリーと呼ばれていた頃（2023年末）から注目はしていましたが（「依存アクテゴリーが面白い」参照）…

モナドや随伴系〈adjunction | adjoint system〉が見つかると良いことあります*1。なので、モナドや随伴系を頑張って探すわけです。相対モナド／相対随伴系は、より一般性がある構造です。もちろん、見つかると良いことあります。しかし、相対モナド／相対随…