A Mechanization of Type Theory