variable-free type theoryの圏論的な解釈について

myuon-myon.hatenablog.com

の続き. いくつか疑問が解消されたのでそれについて.

var-free type theoryについて

syntaxはcontext, type, term, substからなる.
contextはtypeの有限列(通常はvariableとそのtypeの組の列だが, 今回はvariable-freeなのでtypeだけの列になる).
typeはground typeと関数型A → Bとsubstが代入された型(σ[s]の形をしているもの)のいずれか.
termは1と代入された項M[s]のいずれか.
substはidと合成f . gとshift↑とextension<f:subst, M:term>のいずれか.

termは型付けをde Bruijn indexで考える.
term1はcontextの直近のtypeに対応する項とみなす. 例えば, Γ,σ ⊢ 1:σなどである.

substはcontextの間の変換とみなす.
例えばΓ ⊢ id:Γはid(Γ)=Γを表す. また, 合成は通常と逆向きに書くらしい(多分見やすさの都合).
shift↑はindexをすべて1つ加算するような変換とみなす. 例えばΓ,σ ⊢ ↑:Γはindexが上に1つずれるので一番新しいtypeσを忘れるものとみなす.

extensionのtyping ruleは次のようなものである:
Γ ⊢ f:Γ', Γ' ⊢ σ, Γ ⊢ M:σ[f] ⇒ Γ ⊢ <f,M>:Γ',σ

これは, Mによってcontextに新しいtypeを付け加える操作と考えることができる.
あるいは, 変換fをMによって拡張したものとみなしてもよい.

locally cartesian closed categoryでの解釈

ML theoryはLCCCとイイカンジに対応する.
ここではcategory with attributesを使った解釈を使うことにする.

すると上で導入したsyntaxはLCCC(cwa)でいい感じに解釈できる.

contextはobject, contextΓのtypeはΓ-cod morphismとみなす.
type Aをもつtermは, Aに対応するmorphism(shift)のsection.
substはmorphismとみなす.

以上の対応で, 上のsyntaxはcwaの構造で超いい感じになる.

function type→はPi-typeを使って定義するので一旦忘れる. (論文にあるようなcwaを構成するとdependent product/sum, extensional identity typeを持つ)
substidはidentity, 合成はcompositionになる.
shift↑はcwaのcanonical projection operatorになる.
代入された項M[s](M:Γ → Γ,A, s:Γ'→Γ)はpullbackΓ'×Γ,A[s]overΓのUMPから誘導されるmorphism
extension<f,M>はpullbackの対角線にあたるmorphism(Mとfのliftを合成する).
1=<id,id>はpullbackのUMPからつくる.

Set model

上のだけだとよく分からないのでSetで解釈する.

shiftはshift写像<gi,a:A> ~> <gi>
termはこのsectionなので, A型の値の追加, <gi> ~> <gi,a:A>になる. これはa:Aと同一視できる.
代入項に登場するpullbackはΓ'×Γ,A[s] = {(gi', gi, a) | s(gi')=gi, a=M} = {(gi',M)}と同一視できる.
よってM[s]は<gi'> ~> (<gi'>,M)とみなせる.
extensionは<f,t:A> = ↑*f . t ; <gi'> ~> <gi',t> ~> <f(gi'),t>になる.