インスティチューション指標圏の直和と構文構成モナドのクライスリ圏

Σ、Δが指標とする。Expr(Σ) がΣから構成される式の集合だとする。Exprはモナドになるので、指標圏をモナド付きの圏と考える。このモナドのクライスリ圏の反対圏を考えると、これは「定義の圏」となる。それで、定義の圏においては、指標の直和 Σ+Δ が直積を与える。これはなかなかに象徴的な事実だと思った。