具体例
http://fm.mizar.org/contents.html より： Title: Tarski Grothendieck Set Theory Author: Andrzej Trybulec Year: 1990 Identifier: TARSKI PDF URL: http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf Summary: This is the first part of the axiomatics o…
http://www.chimaira.org/archive/MizarLightForHOLLight_miz.ps.pdf より、 :: The drinker's principle reserve x for object; ex x st P x implies for y holds P y proof per cases; suppose A0: ex x st not P x; consider a such that A1: not P a by …
忠実関手と部分圏：忠実だからって埋め込めないよ - 檜山正幸のキマイラ飼育記 メモ編 のより簡単な例。 |C| = {0, 1, 2} C(0, 1) = 2N = {0, 2, 4, ...} C(1, 2) = 3N = {0, 3, 6, ...} 他はidだけか空集合 結合は足し算、idは0とみなす。 |D| = {0} D(0, 0…
グラフとツリーと余反映的部分圏 - 檜山正幸のキマイラ飼育記 上記の例は、基点付き弧状連結空間の被覆空間の類似物だ。空間Xに被覆空間と射影 C(X)→X が定まる。射影が余反映的構造を決める。距離空間と完備距離空間と距離完備化は反映的部分圏の例になる。…
忠実関手 F:C→D がある事と、C⊆D とみなせる事は違う。事例を示す。集合圏Setの対象（つまり集合）のなかから、基数が可算無限であるモノを全て選び出して類Ωを作る。Ω⊆|Set| であるので、Ωを対象類とするSetの充満部分圏が一意に決まる。その圏をω-Setとす…
数量の感覚 - 檜山正幸のキマイラ飼育記 メモ編 の件：ここにまとめておく。足していく（つもり）。 日常的な数量の色々 体重 身長 クラスや会社や組織の人数 価格 移動の距離 移動の時間 ペットボトルの容量 ビルの高さ 部屋やフロアの広さ 荷物の重さ 株価…
参照：よく分からん用語 - 檜山正幸のキマイラ飼育記 メモ編 solve -- テクニカルタームのこともある。goalをsolveする、というし、solved goalともいう。solve this problem とかは日常語だろう。 answer -- ユニフィケーションの結果である束縛をanswerと…
Isabelleの場合： 定理： 実装言語MLのデータ型thmとそのインスタンスを定理と呼び、それに引きずられている。実装レベルでは、たいていの概念がthmデータで表現されているので、なんでも定理（＝thm）となる。 ルール： オブジェクト論理（ユーザー定義の論…
任意のモノイドから作った離散圏 順序モノイドから作ったやせた圏 圏の自己関手の圏（射は自然変換） テンパリー／リーブ圏とその変種 置換の圏（対称の圏）、ブレイドの圏 厳密とは限らないモノイド圏のシークエンス圏
絵算に直す例題に使うつもり。p3, 4 :p.5 :
なるほど、絵の描き方の微妙な差で解釈が変わる - 檜山正幸のキマイラ飼育記 メモ編 で考えたこと。無向グラフの連結成分は、グラフの幾何的実現を考えれば純粋に位相的に定義できる。強連結成分は方向を伴うので位相だけでは定義できない。有向位相（direct…
bookmarkの反応は、「そんな解釈もあるのか」と意外で面白かったりするが、反省と参考になるのは、 「変態グラフを4から3に逆行してaos6に3が入らない意味がわからなくて」 というようなコメント。so-called変態グラフ http://www.chimaira.org/img3/git-hen…
図で、f†は、fに対するコンウェイ（Conway）の不動点演算子。トレースを使って書くと、 f† = Tr(f;Δ) となる。f#はエルゴットの繰り返し演算子。（右にある Tr(∇;f;Δ) は今回関係ない。）f# の表記として、 Tr([ι2A,X, f]) というのがある。ιは標準入射で、[…
ツリーとマトリックスの関係（http://d.hatena.ne.jp/m-hiyama/20121219/1355882745 ）て、マップ型（または配列型）のデータを関数とみなしてのカリー化の等式（同型の式） [I, [J, V]] ＝ [I×J, V] ＝ [J×I, V] ＝ [J, [I, V]] だ。
結合律と左単位律を満たし、右単位律を満たさない例を見つけた。基点付き集合の直和の圏で考えるのだけど、他の圏でも出来るかもしれない。(A, ⊥A), (B, ⊥B) などを基点付き集合圏の対象として、直和は、AとBの集合直和を作って基点⊥Aと⊥Bを同一視した新しい…
Aが有限プレ順序集合として、f:A→N が： fは全単射である。 fの像は、{1, ..., n} の形で、nはAの基数。 順序に関して単調。 このとき、fを単調シリアライゼーションと呼ぶ。次の問題を考える： 与えられたAに対して、単調シリアライゼーションはあるか？ あ…
具体的な強度付きモナドとして、計算関係では何があるか？計算（コンピューティングとソフトウェア）で出てくるモナドは、たいていコレクション系かモノイドスタンピング系。コレクション系： リストモナド + 直積 有限パワーセットモナド + 直積 スタンピン…
最小元を持つ順序集合の圏を考える。射は任意の単調写像で、最小元を保存することは要求しない。集合直積が圏論的直積、単元集合が終対象を与え、単調写像の集合が再び最小元を持つ順序集合になる。この圏では、evと(-)^が定義できてデカルト閉になるが、始…
集合圏かCPOの圏で考えるとして（デカルト閉圏ならいい）、ωは自然数（順序付き）か似たようなモンだとして、Aは勝手な対象。 in:Aω→A out:A→Aω とすると、ストリームIOの雰囲気がする。inとoutの間には通常はなにかしら関係があるが、特に関係は考えないと…
一般的な状況で考えることにして、Cが圏、F:C→C が自己反変関手、δ::Id⇒F;F という自然同型があるとする。このとき、「もとの圏C」と「Fの像となっている圏」は圏同値。具体例は、Cが有限次元ベクトル空間の圏FdVectで、Fが双対空間／写像を対応させる反変関…
改行を「/」で表して行列を書くことにする。W(f) = [1, 0 / f, f+1] がラッピング対応になる。反図式順クライスリ結合を g%f とすると、g%f = g + gf + f となる。gf はgとfの反図式順結合。次が成立する。 W(g%f) = W(g)・W(f) 普通に計算すれば出る。
MをC上のモナドとして、K = Kl(C, M)をクライスリ圏とする。対応(-)--:C→K と (-)∨:K→C を次のように定義する。 X-- = X (f:X→Y)-- = f;εY:X→M(Y) (X→Y in K) X∨ = M(X) (k:X→M(Y))∨ = M(k);μY:M(X)→M(Y) (-)--と(-)∨が実際に関手であることを計算してみる。…
http://www.imsc.res.in/~sunder/canq.pdf ジョーンズ（Vaughan Jones）とサンダー（V.S. Sunder）による図だが、あれは平面タングル（planar tangle）と呼ぶ。だけど、全然実情を表してない言葉だ。平面つっても使うのは円環領域（環帯；annulus, annular d…
[追記] 順序は次のようかな。 MapFO MapFOへの表現、1の3乗根、1の2乗根、自明モノイド＝更新モノイド Nに関する小物圏いろいろ PMapFO PMapFOに関して、二項定理と付点構成（モナド） RelFO RelFOに関して、非決定性写像 RelFOに関して、RelFO = MatΩ(FO) …
関手 KA = λX.A I = λX.X (A×) = λX.A×X (+B) = λX.X + B λX.(X×X + 1) 代数あるいはマグマ自己関手Fに対してF代数という言葉を使うが、あれはFマグマだろう。何の法則もないのだから。K1 = λX.1 という定数関手に対して、K1代数＝K1マグマの圏は点付き集合…
関手SqSq(A) = A×A, Sq(f:A→B) = (f×f:A×A→B×B) 。これは対象[2] = {1, 2} によって共変主表現される。関手DoubleSqの直和版。これは対象[2]のスタンピング。反変ペキ集合関手Pow、これは対象[2]で反変主表現される。反変3値ベキ集合関手[3]により反変主表現…
CがK-線形圏だとして、RがK-多元環（代数）のとき、テンソル積R(×)Cが定義できる（前のエントリーに書いた）。もっと一般に、線形圏CとDのテンソル積が、|C|×|D|上に、 (C(×)D)( (A, B), (A', B') ) = C(A, A')(×)D(B, B') として定義できる。単一の多元環と…
/* MapFO.js -- Map Category over Finite Ordinals */// 整数の区間を作る // （一般的にも使えそう） function seq(n, m) { // n, mは整数、n ≦ m と仮定 var a = new Array(); for (var i = 0; i <= (m - n); i++) { a[i] = n + i; } return a; }// 名前…
/* HSCat.js -- Hiragana Shiritori Category *//* * 一般的な文字列処理関数 */// 文字列の連接 function concat(s, t) { // s, t は文字列と仮定 return String.prototype.concat.call(s, t); }// 文字列の最初の文字（ただし文字番号が返る） function fi…
リストモナド＝列モナドの代数は、a:A*→A だから、任意のnに対するn講演算を備えた集合。a:A+→A なら、0項演算（特別な定数）はない。Idモナド（自明モナド）の代数は任意の自己射になる。Rに対して、a:R*→Rに対して、a(空) = 7, その他は平均値の2倍とか定…
