ループを無視していいのか？

Samson Abramsky, Ross Duncan "A categorical quantum logic"（http://www.mathstat.dal.ca/~selinger/qpl2004/PDFS/02Abramsky-Duncan.pdf）に次のように書いてある。

An LCCB2 sequent is of the form
 Γ |- Δ; [L]
where Γ, Δ are lists of formulae and L is a multiset of loops.
The inclusion of the loops in the definition of sequent is slightly

misleading: strictly the loop sets are a proof decoration rather than

a property of the sequents themselves. For this reason two sequents

are defined to be equal if they differ only by loops.

しかし、コンパクト閉圏でもテンパリー／リーブ圏でも、これは違う気がする。つまり、ループも証明図の一部と考えたほうがいいだろう。少なくとも幾何学的には意味がある。論理が幾何の一部を捨てているってことだろう、たぶん。