Categoricity and quantifier elimination for intuitionistic theories