Categories with attributes (cwa) - ヒビルテ(2008-08-02)λ. Categories with attributes (cwa) 依存型とcatamorphism の話を書くために、まずは依存型を持つ体系の圏論的なモデルとして Categories with attributes を導入する。 Categories with attributes Category with attributes (cwa) は依存型を持つ計算体系の圏論的なモデルとしてよく使われる圏で、以下の構成要素と条件からなる。 圏 C 終対象 1∈|C| 前層 Fam : Cop → Set 射に対する作用については S[f] := Fam(f)(S) という記法を用いる。 任意の Γ∈|C| と S∈Fam(Γ) に対して、Γ・S ∈ |C| という対象と射 πS : Γ・S → Γ が存在する 記法を濫用して πS のことを、単に S と書くことがある。 任意の射 f
fam.cx
8.4 対応関係の拡張
1 述語論理とその意味論
DependentlyTypedProgramming2009 - Lectures of IPL
