現在作業中のメモ。
形容詞「ドブ板」 - 檜山正幸のキマイラ飼育記 (はてな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 )