あつらえたラムダ計算

現在作業中のメモ。

形容詞「ドブ板」 - 檜山正幸のキマイラ飼育記 (はてなBlog) -- ドブ板計算 (苦笑)。

対象がAが定義する、右からのA-掛け算関手 (-)□A と A-累乗関手 [A, -] が定義する随伴系の単位と余単位を定義する。そのために、ラムダ計算をテーラーメイドした。

εX:hom(A, X)□A→X
 := (λ0(f, i)∈hom(A, X)□A. f(i) ∈X
     AND
     λ1(f→f', i)∈hom(A, X)□A. f(i)→f'(i) ∈X
     OR
     λ1(f, i→i')∈hom(A, X)□A. f(i)→f(i') ∈X
    )

ηX:X→hom(A, X□A)
 := (λ0k∈X.
       (λ0i∈A. (k, i) ∈X□A
        AND
        λ1(i→i')∈A. ((i→i'), k) ∈X□A
       )
     AND
     λ1(k→k')∈X. λ01i∈A. ((i→i'), k) ∈X□A
    )