圏の定義

本編のコレだけど、部分関数／部分演算を等式的一階述語論理でどう扱うかの例題として面白いかもしれない。次のような体系も考えるといいかも。

• domu（id(dom(-))に対応）とcoduを持つ体系
• 「…が存在する」を意味する述語E(-)を持つ体系