Re: Is cut semantical?

From: Michael Barr <barr@triples.math.mcgill.ca> I should clarify. Proofs with cuts correspond to composable paths. If you like, to proofs in the graph (or free category) of a category. Yes, the free thing on the syntax you're trying to model usually does the job, e.g. the Lindenbaum algebra. But is there any mathematical object arising in nature that works like proofs with cut, the way natural transformations do for cut-free proofs? It is somewhat magical that natural transformations match proofs in this way when they do, and reassuring when they don't: they're letting you know they're alive and require maintenance, unlike free things which are dead and therefore maintenance-free. Vaughan