トップ «前の日記(2008-08-04) 最新 次の日記(2008-08-06)» 月表示 編集

日々の流転


2008-08-05 [長年日記]

λ. Categories with families

Categories with attributes を使って色々書こうとしてたけど、Categories with attributes とは別に Categories with families というのがあって、こっちの方が扱いやすいようだ。しょぼーん。

一応、定義とかをメモしておく。

圏 Fam(C)

対象 A=(A0, A1)
集合 A0 と A0 によって添え字付けられたCの対象の族 {A1a}a∈A0 の組
射 f=(f0,f1) : A→B
関数 f0 : A0 → B0 と、Cの射の族 {f1a : A1a → B1f0(a)}a∈A0 の組

ちなみに、Fam(C)から第一成分を射影する関手 Fam(C)→Set は、Bart Jacobs の Categorical Type Theory で「"Family fibration" Fam(C)→Sets」と呼ばれているもの。

comprehension

関手 F=(Ty,Tm) : Cop→Fam(Set) と Γ∈|C| と σ=Ty(Γ) が与えられているとする。 σ の comprehension は以下の構成要素と条件からなる。

  • Γ・σ ∈ |C| と
  • p(σ) : Γ・σ → Γ
  • vσ : Tm(Γ・σ, σ[p(σ)])
  • 任意の f : Δ→Γ と M∈Tm(σ[f]) 対して、p(σ)∘<f,M>σ = f かつ vσ[<f,M>σ] = M であるような射 <f,M>σ : Δ → Γ・σ が一意に存在。

Categories with families

Categories with families (CwF) は以下の構成要素と条件からなる。

  • 圏 C
  • 終対象 1∈|C|
  • 関手 F=(Ty,Tm) : Cop→Fam(Set)
  • Γ∈|C| と σ∈Ty(Γ) に対して comprehension が存在

Categories with Attributes との関係

.