Exchange Rule

In logic and type theory, the exchange rule is a Structural Rule that lets you permute elements of the context.

For systems based off of Natural Deduction, exchange rules take the form of

$\par\frac{\Gamma_{1},x:X,\Gamma_{2},y:Y,\Gamma_{3}\vdash e:A}{\Gamma_{1},y:Y,% \Gamma_{2},x:X,\Gamma_{3}\vdash e:A}\\$

For Sequent Calculi, we need to add both Left and Right Rules, ala

	$\displaystyle\frac{\Gamma_{1},x:X,\Gamma_{2},y:Y,\Gamma_{3}\vdash\Delta}{% \Gamma_{1},y:Y,\Gamma_{2},x:X,\Gamma_{3}\vdash\Delta}$
	$\displaystyle\frac{\Gamma\vdash\Delta_{1},x:X,\Delta_{2},y:Y,\Delta_{3}}{% \Gamma\vdash\Delta_{1},y:Y,\Delta_{2},x:X,\Delta_{3}}$

An equivalent presentation involves adding in Permutations to the calculus of Substitutions, which makes the resulting Category of Contexts a Symmetric Monoidal Category.

Note that exchange is a bit tricky in the presence of Dependent Types, as applying an exchange rule can make things ill-typed.