ウエス計算（Uesu calculus） #1

とりあえず、はじめよう。

Cは有限積を持つ圏。Vが（集合とは限らない）変数の集まり。#:V→|C|が、割り当て。#(x)∈|C|を「xの変域」（もちろん、#を仮定して）と呼ぶ。

Cの適当な拡張圏C'（C=C'でもよい）があって、Vの重複を持たない有限列Xに対して、#:USeq(V)→|C'|があって次を満たすとする。

1. X=(x1, ..., xn)として、#(X)≒#(x1)×...×#(xn)
2. 特に#( ())≒1、#( (x))≒#(x)

事情を明確にするため、Vの有限列Xに対して、ι_X:#(X)≒→#(x1)×...×#(xn)を同型だとする。ι₍₎、ι_(x)などが1や#(x)との同型を与える。以上の(C, V, #, C', #, ι)の組をC上の変数系と呼ぶ。記号#は、V→|C|とUSeq(V)→|C'|の両方の意味で使っている。