情報隠蔽〈information hiding〉＝カプセル化〈capsulation〉＝ボクシング＝パッケージング 情報公開〈Information disclosure〉＝脱カプセル化〈de-capsulation〉＝アンボクシング＝アンパッケージング パターン＝テンプレート＝ワイヤリングスキーマ カプ…

Σ〈$`\Sigma`$〉なんらかの意味の指標、D〈$`D`$〉はドクトリンだとして、$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\In}{ \text{ in } } \newcommand{\mrm}[1]{ \mathrm{#1} } %`$$`\quad \cat{C} = \mrm{Th}^D(\Sigma)`$とする。$`\cat{E}`$ を同…

フラットコンステレーション＝ストリング図テンプレート⊇ワイヤリング図 ソリッドディスク＝ストリング図⊇無ノード・ワイヤリング図＝スパイダー図 外サークル＝ストリング図のキャンバス境界 内サークル達＝ストリング図テンプレートのスロット境界達 中間…

右の欄はローヴェアの代数セオリー。 アリーナ コンステレーション 代数指標 カローラ テンプレート オペレーション アリーナ テンプレートキット 指標 ツリー コンステレーション 項 フォレスト コンステレーションキット 割り当て〈代入〉系 リーフ スロッ…

コンテナをアリーナ＝カローラ・フォレストで図示するとして： ツリーをグラフと見るとき、通常グラフ解釈かオープングラフ解釈か？ リーフをどう描くか？ ドット、アロー、ワイヤー ルートをどう描くか？ ドット、アロー、ワイヤー ツリーとルートを別物と…

大きかも知れない圏の2-圏 順序集合の圏 余完備な余デカルト圏 順序完備なミート半束 余連続な自己関手 連続な自己関数 自然変換 関数順序 自己関手のランベック代数 自己単調関数の劣不動点 モナド 閉包作用素 モナドのアイレンベルク／ムーア代数 閉包作用…

困っている。 何がプレーンレンズ〈バニラレンズ〉か分からない。 元祖レンズの有法則／無法則は、まーハッキリしている。 単相レンズ〈monomorphic lens〉と双相レンズ〈ニ相レンズ | bimorphic lens〉の区別はあるが、一般的とも言えない。ヘッジーズ〈Hea…

終対象への唯一射や、単位対象への構造射 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 のように英字と数字の並び、…

Quoraの「TypeScriptって気持ち悪くないですか？」なる質問に、以下のコードと共に： Aだと変数aに代入するときにエラーにならないのですが、Bだと変数aに代入するときに型のエラーになるんです。 え、なんで？同じ動きしているはずなのに。 const getA = ()…

次のような対応があると思う。 テレスコープ ←→ フォレスト テレスコープのシグマ構成圏の対象 ←→ フォレストのパス テレスコープのシグマ構成圏の対象集合 ←→ フォレストのパス集合 テレスコープに関して、レベルk（k - 0, 1, ...）のベース圏を考える。レ…

カリー同型とフビニ定理は切っても切れない。フビニ定理は、カリー同型で互いに移る高階関数と多変数関数の積分が一致することを主張している。同様に、依存カリー同型と依存フビニ定理は切っても切れない。依存フビニ定理は、カリー同型で互いに移る高階依…

カリー同型は、複関数〈multifunction | 多重関数 | 多変数関数〉と高階関数〈higher-order function〉との1：1対応を与える。同様に、依存カリー同型は、依存複関数と依存高階関数のあいだの対応を与える。さらに、関数を関手に一般化するると、依存複関手…

靴はオンラインでは書いにくい、と思っていたが、気に入った靴を決め打ちにして、同じ型番のものを買い続ければいいのか。「いつも同じ靴」現象は起きるが、楽ちんさが勝る。

テレスコープとグロタンディーク構成とグロタンディーク／フビニの定理の関係：indexed thing = indexed family of things を単にファミリーと呼ぶ。インデックス付き圏もファミリーになる。テレスコープはファミリーに関して定義できる。テレスコープの第1…

顔負け 貫禄負け 気圧される 圧倒される 威圧される 威嚇される 怖気づく 萎縮する 恐怖を感じる 親しみを持てない 劣勢に立たされる 例えば：$`{\displaystyle \int_{x = a}^b \frac{df}{dx}(x)\, dx = \Big[ f(x) \Big]_{x = a}^b}`$

くどいが： 一貫性法則は命題である。 一貫性定理は、一貫性法則という命題が真であると保証している定理（証明付き） 法則は単なる命題で、定理は真である保証。一貫性法則という命題を公理として要求するときは一貫性要求。「一貫性公理」と言うとバランス…