How can an existential type be defined in terms of universal type? In Types and Programming Languages by Pierce,  how does the following achieve the definition of an existential type  in terms of universal type, by polymorphic version of Church encoding of pairs?


  24.3 Encoding Existentials
  
  The encoding of pairs as a polymorphic type in §23.4 suggests a
  similar encoding for existential types in terms of universal types,
  using the intuition that an element of an existential type is a pair
  of a type and a value:

{∃X,T} := ∀Y. (∀X. T→Y) → Y.

  
  That is, an existential package is thought of as a data value that,
  given a result type and a continuation, calls the continuation to
  yield a ﬁnal result. The continuation takes two arguments—a type X and
  a value of type T—and uses them in computing the ﬁnal result.


To complete the quote, the polymorphic version of Church encoding of pairs of numbers is given in Exercise 23.4.8 (p349 p546):

pairNat = λn1:CNat. λn2:CNat.
λX. λf:CNat→CNat→X. f n1 n2;
fstNat = λp:PairNat. p [CNat] (λn1:CNat. λn2:CNat. n1);
sndNat = λp:PairNat. p [CNat] (λn1:CNat. λn2:CNat. n2);


which is further generalized to pairs of elements of any types, on p352


  we use the abbreviation Pair X Y (generalizing the PairNat type from
  Exercise 23.4.8) for the Church encoding of pairs with ﬁrst component
  of type X and second component of type Y:

Pair X Y = ∀R. (X→Y→R) → R;

  
  The operations on pairs are simple generalizations of the operations
  on the type PairNat above:

&gt; pair : ∀X. ∀Y. X → Y → Pair X Y
fst : ∀X. ∀Y. Pair X Y → X
snd : ∀X. ∀Y. Pair X Y → Y



Thanks.
As a general recipe, to figure out how to encode a type A, write down

∀Z . (A → Z) → Z


and massage it to something that does not involve A, using basic isomorphisms, such as currying and uncurrying. For example, if we plug in A := X + Y we get:

∀ Z . (X + Y → Z) → Z           ≅
∀ Z . (X → Z) × (Y → Z) → Z     ≅
∀ Z . (X → Z) → (Y → Z) → Z


You can also read the above lines as a sequence of logical equivalences. So this gives us the encoding of X + Y in terms of the universal quantifier.

I do not understand why in your question you speak about existential types, but since you do, it is worth explaining the encoding of ∃ X . B(X) in terms of ∀ this way:

∀ Z . ((∃ X . B(X)) → Z) → Z    ≅
∀ Z . (∀ X . (B(X) → Z)) → Z


Again, you can read the equivalence either as a type isomorphism or a logical equivalence in logic, using the fact that $(\exists x . \phi(x)) \Rightarrow \psi$ is equivalent to $\forall x . (\phi(x) \Rightarrow \psi))$.