2022-09-08から1日間の記事一覧

唯一射と対角射

終対象への唯一射や、単位対象への構造射 delete morphism descarder eraser discharger terminal morphism vanishing morphism bang garbage morphism(gs圏のこじつけ) counit もう一方の射は、 comultiplication duplicator copy morphism diagonal morp…

続・表計算

そうそう、セルに型が付くのだった。セルに型フィールドと値フィールドがある。特定番地のセルのフィールドに値が入っていることを$`\quad \text{A2.Val} = 7\\ \quad \text{A2.Typ} = {\bf N} %`$まとめて$`\quad \text{A2} = (7 : {\bf Nat})`$次の機能が…

依存関数

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

例え話に表計算

ヒエー、僕は使ったことない。 表計算ソフト〈スプレッドシート〉が便利なのは、入力に対する自動計算/自動再計算をやってくれるから。 高機能かつDomainSpecificな電卓〈カリキュレーター〉として使える。 セル番地は A1, C30 のように英字と数字の並び、…