We present {\em axioms} on models of system F, which are sufficient  
to show {\em full completeness} for {\em ML-polymorphic types}.
These axioms are given for {\em hyperdoctrine} models, which arise as
{\em adjoint models}, i.e. {\em co-Kleisli categories} of suitable 
{\em linear categories}.  
Our axiomatization consists of two crucial steps.
First, we axiomatize the fact that  every relevant morphism in the mode
generates, under {\em decomposition}, a  possibly {\em infinite} typed 
B\"ohm tree. 
Then, we introduce an axiom which rules out infinite trees from the model. 
Finally, we discuss the necessity of the axioms.