日々の流転

λ. Categories with families

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

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

圏 Fam(C)

対象 A=(A0, A1)

集合 A0 と A0 によって添え字付けられたCの対象の族 {A1_a}_a∈A0 の組

射 f=(f0,f1) : A→B

関数 f0 : A0 → B0 と、Cの射の族 {f1_a : A1_a → B1_f0(a)}_a∈A0 の組

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

comprehension

関手 F=(Ty,Tm) : C^op→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) : C^op→Fam(Set)
• Γ∈|C| と σ∈Ty(Γ) に対して comprehension が存在

Categories with Attributes との関係

.