A Category of Classical Proofs

from blog Home on consequently.org, | ↗ original
Abstract: I show that the cut-free proof terms defined in my paper “Proof Terms for Classical Derivations” form a well-behaved category. The talk is intended to be accessible enough for those who don’t know any category theory to follow along. I show that the category is not Cartesian – and that we’d be wrong to expect to be. It has no products...