Natural Models of Type Theory