ハロ多圏とコア圏

結局、ハロ多圏の多射が項であって、コア圏の射が値だな。多射は図形だが、それは構文的な存在でもあり、項書き換えの対象となる。つまり、書き換え操作が計算であり2-多射でもある。計算の結果を対応さると、式と計算の意味論ができて、多圏のほうには、2-多射を使った1-同値が定義できるってことだろう。