型理論

依存関数

型ファミリーのセクション $`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…

指標と型クラス 1

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| のときが総称型…

*-as-Typesパラダイム

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…

型の縦階層と横階層

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