# Mapping a free variable of type A to a cartesian closed category

In From Lambda Calculus to Cartesian Closed Categories, the author explains the interpretation of lambda calculus in cartesian closed category and at one point he explains how a term representing a free variable of type A is mapped to the cartesian closed category as follow:

 [Γ x:A :- x:A] = π2 : ([Γ ] × [A]) → [A]

(A term which is a free
variable of type A is an arrow from the product of Γ and the type object A to A;
That is, an unknown value of type A is some arrow whose start point will be
inferred by the continued interpretation of gamma, and which ends at A.
So this is going to be an arrow from either unit or a parameter type to A -
which is a statement that this expression evaluates to a value of type A.)


I appreciate if someone can elaborate further on what the author means, perhaps with an example, since I am a newbie to category theory.

In the interpretation of the simply-typed $$\lambda$$-calculus in a cartesian-closed category, contexts $$\Gamma$$ and types $$A$$ are interpreted as objects $$⟦\Gamma⟧$$ and $$⟦A⟧$$ (types being equivalent to one-variable contexts), while a term $$\Gamma \vdash t : A$$ is interpreted as a morphism $$⟦t⟧ : ⟦\Gamma⟧ \to ⟦A⟧$$.
Context extension is represented by taking the product in the cartesian-closed category, that is: $$⟦\Gamma, x : A⟧ = ⟦\Gamma⟧ \times ⟦A⟧$$. We want to form the projection of the variable $$x : A$$, which is represented by a morphism $$⟦x⟧ : ⟦\Gamma, x : A⟧ \to ⟦A⟧$$, which by definition is a morphism $$⟦x⟧ : ⟦\Gamma⟧ \times ⟦A⟧ \to ⟦A⟧$$. There's one obvious choice here: to project the second component of the product. Taking $$⟦x⟧ = \pi_2$$ gives us a term of the correct type and it satisfies the expected properties.
In general, contexts (represented by lists of variables in the type theory) are represented by products of types in the cartesian-closed category, and the term corresponding to the $$i^\text{th}$$ variable is given by the $$i^\text{th}$$ projection from the product, $$\pi_i$$.