Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing