u = undefined として、記号の乱用で u = {u}。ブラケット内の数値はランクが減少する量。 ●opt-right A ⊆ B+u [u!∈A] -----------[-1] A ⊆ B●opt-both A+u ⊆ B+u [u!∈A, u!∈B] -----------[-2] A ⊆ B●object object {pi: Ai} ⊆ object {pi: Bi} -----------…

Catyの型推論のために、分解還元法というのを考えた。シーケント計算とタブローの中間のような感じのもの。推論は逆向きに（結論から仮定へと）行われるので、次の用語を導入する。 分解図 -- 推論図（1ステップ）の逆 還元図 -- 証明図（nステップ）の逆 シ…

最小元を持つ順序集合の圏を考える。射は任意の単調写像で、最小元を保存することは要求しない。集合直積が圏論的直積、単元集合が終対象を与え、単調写像の集合が再び最小元を持つ順序集合になる。この圏では、evと(-)^が定義できてデカルト閉になるが、始…