非厳密な多圏は難しい

ラムダ計算の重箱の隅(?)：タプルと成分 - 檜山正幸のキマイラ飼育記 メモ編 ：

やっぱり多圏の議論をしないとどうにもならない、と感じる。
...
重箱の隅でもないな、これは。

難しい問題が持ち上げる。

Cが厳密モノイド圏のとき、それから厳密多圏Poly(C)を作れる。この手順は比較的簡単だし、できた多圏Poly(C)も扱いやすい。しかし、Cが厳密でない時は、Poly(C)の作り方がハッキリしない。話を簡単にするには、Cからモノイド圏の厳密化をして、その後で多圏を作ればよい。

ところが、ラムダ計算のモデルとしてCがあるとき、Cの厳密化とラムダ項の構文側との関係が問題になる。

モノイド圏の厳密化によって、ラムダ項の項書き換えシステム側でどう対処して、意味論写像をどう変更するかをキチンと定義しなくてはならない。

別な方法として、Cの厳密化をしないで、多圏を作る方法があるが、これは難しい。というか、見当がつかない。