Re: Is cut semantical?

Maybe I am being naive, but I always thought that cuts were equivalent to composing arrows. The fact that in getting an arrow A --> B, you could take arbitrary paths A --> C --> B corresponds to the unbounded nature of proofs with cut. Of course, if you can calculate Hom(A,B) directly, this is all irrelevant. Mike