kernel/file.erl に -spec が使われている。

半環RにNが作用しているとき、融合和（amalgamated sum）が定義できる。半直和という感じの構成だ。(R, +, ・, z, u)が半環（zは零、uは単位）とする。x∈Rに対して、 0△x = x n△x = u + .. + u + x（uがn個） 0*x = z n*x = x + ... + x（xがn個） として作…

これは気付かなかった -- コロンブスの卵。圏Cの骨格を[C]と書くことにする。[C]はとりあえずは単なる集合。Eを有限極限を持つ圏で、選択された直積×を持つとする。A, B∈|E|に対して、A×Bは決まる。スライス圏E/(A×B)も定義できる。骨格 [E/(A×B)] が、スパ…

Rがなんらかの代数構造で、代数構造を保存する同値関係を合同（congruence）と呼ぶ。これは曖昧すぎるが、個々のケースでは厳密な定義ができる。たとえば、モノイド上の合同は： 〜は同値関係 a〜a'、bからb' ならば ab〜a'b' 〜がM上の合同なら、商M/〜を再…

「圏の骨格」はある程度は使われている用語。「圏の本質」は定かではない。だが、圏が「本質的に小さい」（essentially small; 綴り字注意）は使われる。その定義は、小さい圏と圏同値になることである。局所小で骨格も小さい圏Cは、骨格集合Skel(C)からのセ…

n-同値の続きの話。可換性や結合性などの性質は、等式を使った法則として表現される。等式は0-同値による関係式だから、0-法則と呼ぶ。1-同値＝同型による法則は1-法則と呼んでいいだろう。1-法則の実体は同型射なので、可逆な1-セルとなる。1-法則を与える1…

骨格か本質か - 檜山正幸のキマイラ飼育記 メモ編 射に対しても同型を定義すれば、骨格に圏の構造を与えられそうだ（これは要確認）。 これはウソだが、骨格はグラフ構造を持つ。以下に述べる。記号≡と〜を使い分ける。idを対象と同じ記号で略記することあり…

associator, unitorはけっこういい用語法だと思っていた。これに合わせると、分配法則を記述する構造同型射（structure isomorphism）をdistributorと呼べばいいのだ、ぬあんと、プロ関手（副関手、profunctor）を、distributorとも呼ぶのであった。そもそも…