日々の流転

λ. cwaでのユニット型の解釈

Categories with attributes (cwa) で cwa の簡単な説明を書いたので、今度は cwa で幾つかの基本的な型を扱ってみることに。 まずは一番簡単と思われるユニット型を。

構成規則と導入規則

通常扱う構成規則と導入規則は以下のような形になっている。

---------------
Γ ├ Unit set
Γ ├ () : Unit

これだと任意のΓについて考えなければならず面倒くさいが、実際のところはそれらの解釈はΓが空である場合からweakeningによって得たものと等しくなければならないので、Γを空の場合に限定した以下の規則を考えることにする。

--------------
├ Unit set
├ () : Unit

これはそれぞれ Unit ∈ Fam(1) と () ∈ Tm(1, Unit) で解釈される。 Γが空でない場合は、weakening -[!_Γ] を使って Unit[!_Γ]∈Fam(Γ) と ()[!_Γ]∈Tm(Γ, Unit[!_Γ]) で解釈できる。

除去規則

お次は除去規則で、通常の除去規則はこんな形をしている。

Γ, x : Unit ├ P set
Γ ├ M : P[x:=()]
Γ ├ N : Unit
--------------------------------
Γ ├ elim(P,M,N) : P[x:=N]
Γ ├ elim(P,M,())=M : P[x:=()]

ただ、これも少し扱いにくいので、少し変えて、以下のような規則を考える。

Γ, x : Unit ├ P[x] set
Γ ├ M : P[()]
---------------------------------------------
Γ, x : Unit ├ elim(P,M)[x] : P[x]
Γ ├ elim(P,M0)[()] = M : P[()]

これの解釈は、 任意の P ∈ Fam(Γ・Unit[!_Γ]) と M ∈ Tm(Γ, P[()[!_Γ]]) に対して、 elim(C,M) ∈ Tm(Γ・Unit[!_Γ], P) が存在し、 elim(C,M)[()[!_Γ]] = M ∈ Tm(Γ, P[()[!_Γ]]) が成り立つということになる。 図で書くと以下のような感じになる。