メリス／ジルバーガーの次の論文をチラ見・拾い読みしました。 [MZ13-][MZ15] Title: Functors are Type Refinement Systems Authors: Paul-André Melliès, Noam Zeilberger Year: 2015 Pages: 14p URL: https://www.irif.fr/~mellies/papers/functors-are-t…
「判断形式を普通に書く」より： 型理論の判断形式を使うと、非常に簡潔に書けます。しかし、簡潔さの代償として、多くの情報を暗黙化します。コラリア／ディ-リベールティも簡潔な記述を目指しているので、えげつない「記号の乱用、短縮記法、完全な省略」…
前回の記事「判断形式を普通に書く」で、コラリア／ディ-リベールティの次の論文を参照しました。 [CL21-24] Title: Context, Judgement, Deduction Authors: Greta Coraglia, Ivan Di Liberti Submitted: 17 Nov 2021 (v1), 1 Nov 2024 (v3) Pages: 61p URL…
型理論の人々は「判断形式で書かないと死んでしまう」のでしょうか？ そして、判断形式にターンスタイル（'$`\vdash`$'）とコロン（'$`:`$'）以外使ったら死んでしまう」のでしょうか？ターンスタイルとコロンへの執着は、もはや「好みの問題」の域を超えて…
圏論的概念は、可換図式やペースティング図を使って定義や記述がされます。テキスト構文で書けないわけではないですが、矢鱈に煩雑になります。現実的には、図式なしではやっていけません。この記事では、図式による定義を、明確かつ簡潔に書くためのフォー…
ヒルベルトのイプシロン記号は、集合からその要素を気まぐれに（まったく予測できないスタイルで）取り出す操作です。ヒルベルトのイプシロン記号が便利な場面や必須な場面があります。しかし、ヒルベルトのイプシロン記号に空集合を渡したときの挙動がよく…
形式化された議論であれ非形式的〈インフォーマル〉な議論であれ、命題と規則を区別する必要はあります。「型理論と論理： 非形式シーケント記法 // 規則は命題ではないのだが」において、規則は命題ではないと言ったのですが、混同されるのはそれなりの理由…
あー、そういうことかぁ！僕は、用語の語源にあまりこだわらないので、「包括圏」の語源は知らなかったし、調べることもしませんでした。「なんでか知らんけど、『包括圏』って呼ぶのね」で済ませていました。語源や逸話を知らないと概念を理解できないわけ…
「型理論周辺、何で混乱するのか？」において： 型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです 地雷原になってしまう大きな理由に、ターンスタイル記号 '$`\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}…
