A cartesian closed category in Martin-Loef's intuitionistic type theory