述語という概念により、Propositions-as-Functions なのだが、$`\mathrm{Pred}(X)`$ を型ファミリー $`\mathrm{PRED}(X)`$ に持ち上げる。すると： 真偽値は、型になる。 述語は、型ファミリーになる。 真偽値／述語を型／型ファミリーに持ち上げることによ…

第一段階： 型＝集合、インスタンス＝要素、関数も（関数空間型の）インスタンス 第二段階： 型＝集合、型ファミリー＝関数、型ファミリーはインスタンスとは別 第三段階： 型は特殊な型ファミリー、インスタンス＝セクション 第四段階： 型＝型ファミリー …

型理論 論理 集合圏 Set 論理圏 Logic 型のポイントインスタンス 命題の証拠 引数リスト 前提〈仮定 | 仮説〉リスト 関数 定理 戻り値型 結論命題 関数の計算 定理の証明 関数のプロファイル 定理のステートメント トップダウン関数定義 バックワード・リー…

$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\ckw}[1]{ {\bf \text{ #1 }} } `$ $`\text{普通}`$ $`\text{丁寧}`$ $`\Gamma \vdash `$ $`\Vdash_\mrm{wf} \Gamma \ckw{ctx}`$ $`\Gamma \vdash A`$ $`\Gamma \vdash_\mrm{wf} A \ckw{type}`$ $`\Gamma …

次の4つは同じこと。 x は、n重〈n-fold〉の繰り返しインデックス付き圏の対象である。 x は、n重〈n-fold〉の繰り返しファイブレーション・スライス圏の対象である。 x は、長さnのファイブレーション・パス〈グロタンディーク・テレスコープ〉である。 x …

拡張包括構造を持った圏が、カートメル構造／カートメル性〈Cartmell property〉を持つとは、$`\newcommand{\cat}[1]{\mathcal{#1}}`$ |$`\cat{C}`$| 上の長さ関数 $`\ell :|\cat{C}| \to {\bf N}`$ がある。 長さが 0 の対象は終対象に限る。終対象はひとつ…

型ファミリーのセクション $`x \in \mathrm{Sect}(\pi:\Sigma(I, F) \to I) = \Pi(I, F)`$ 関数型ファミリーのセクション $`x \in \mathrm{Sect}(\pi:\Sigma(I, [F, G]) \to I) = \Pi(I, [F, G])`$ 一番は依存リストで、ニ番はインデックス付き関数〈indexed…

長谷川真人さんの "Classical Linear Logic of Implications"https://www.kurims.kyoto-u.ac.jp/~hassei/papers/clli.pdf ：加法的〈非線形〉コンテキストと乗法的〈線形〉コンテキストを持つ型判断〈typing judgement〉$`\quad \Gamma ;\Delta \vdash M:\si…

data Tree a = Leaf a | Tree (Tree a) (Tree a) 値コンストラクタ、型コンストラクタ、型が紛らわしいという例。値コンストラクタをタグだと考えると： type Tree<A> = @Leaf A | @Tree [Tree<A>, Tree<A>] タグ @Leaf, @Tree に対応する値コンストラクタを ^Leaf, ^</a></a></a>…

用法1 用法2 用法3 シグマ型 依存ペア型 依存積型 依存和型 パイ型 依存関数型 依存指数型 依存積型 description _ procedure Sigma from a Type A and a Family (F : A → |Set|) produces a Type S { // 省略 } procedure Pi from a Type A and a Family (F…

Twitterでつぶやいていた内容の一部をメモにしておこう。無名指標と入れ子指標無名指標または指標リテラルは、sig {...} の形で書く。 sig { sort U operation e:ε → U operation m:(U, U) → U }これはモノイド指標（monoidal signature、「モノイドの指標」…

型カインドの定義は次にある。 https://m-hiyama.hatenablog.com/entry/2020/10/21/175259 これだと、単に「型の集合」だが、排他的型カインドという概念を入れないとまずいな。排他的型カインドと型ファミリー（型でインデックスされた型の族）をしっかり区…

次は同義語 多相型 総称型 型構成子 パラメータ付き型 インデックス付き型 型ファミリー 適切な言葉は型値関数、使うのは型ファミリーにする。型ファミリーとは、Xを集合として、F:X → |C| という写像。Cの対象を型と呼べば、型値関数。X⊆|C| のときが総称型…

Sets-as-Types, Functions-as-Terms Algebra-as-Types, Morphisms-as-Terms Coalgebra-as-Types, Morphisms-as-Terms Categories-as-Types, Functors-as-Terms Propositions-as-Types, Proofs-as-Terms Sets-as-Types と (Co)Algebras-as-Types は、単純型＝…

後で追加修正するかも。指標の一覧： 名前 提供記号 ひとこと Magma * 乗法記号使ったマグマ UnitalMagma *, 1 単位的マグマ MonoidAste *, 1 モノイド MonoidPlus +, 0 モノイド Group *, 1, ~ 群 AbGroupPlus +, 0, - アーベル群 Ring +, 0, -, *, 1 可換…

あまりにも車輪の再発明が凄まじ過ぎて、用法や雰囲気（だけ）が違う同義語が山のようだ。少し整理しておく。基本レベルとは圏の次元を基準としたレイヤー番号のこと。基本レベルが1の存在物〈スタッフ〉はレイヤー1にいて、存在物の圏論的次元は1。 基本レ…

_R のような下線で始まる語は太字の代替で、固有名詞（特定インスタンスを指す名前）となる。次元ごとに付けるキーワードは恣意的なので括弧に入れることにした。 1-sinature movable { 0(sort) S in _Set 1(mathod) moveBy:S×_R→S in _Set 2(equation) assc…

型階層を考える上で、型を分類する必要がある。 型と種 無構造型（集合）と構造付き型 単純型〈基本型 | 組み込み型〉と複合型〈構成型 | 複雑型〉 全域型と部分型〈制約型〉 型と種は縦階層。縦階層は、オブジェクトレベル、メタレベル、メタメタレベルのよ…