In Types and Programming Languages by Pierce the author talks about how permuting a typing environment does not affect bindings from variables to types. Specifically he states:
The first structural lemma tells us that we may permute the elements of a context, as convenient, without changing the set of typing statements that can be derived under it.
He then presents the following lemma:
Lemma[Permutation]: If Γ ⊢ t : T and ∆ is a permutation of Γ, then ∆ ⊢ t : T. Moreover, the latter derivation has the same depth as the former.
$\Gamma$ is a function mapping variables to types, or equivalently a set of pairs of variables and types. A permutation is depending on the definition either a tuple of elements from a given set or a mapping from that set to itself. So in either case a permutation $\Delta$ of a function $\Gamma$ is of a different type than $\Gamma$ itself. But then the Lemma makes little sense, as it treats $\Delta$ just like $\Gamma$ in regard to their type.
So I must be misunderstanding the author here, who unfortunately does not clarify what he means by permutation.
What does he mean by it then and how is it related to the above two definitions of permutation?
A context $\Gamma$ is not a set of pairs of variables and types, it is a list of pairs of variables and types. So $\Gamma := (x:A, y: B, z:C)$ is a context.
(Looking at Pierce's book, he uses the term sequence rather than list.)
$\Delta:= (z:C,y:B,x:A)$ is also a context, but since contexts are lists and not sets, it is a different context than $\Gamma.$ However, since it contains the same variables and types in a different order, $\Delta$ is a permutation of $\Gamma.$
This is what is meant by the terminology. The lemma then just says that contexts that are permutations of one another are effectively equivalent, as one might expect.