Văn bản này: Correctness of automatic differentiation via diffeologies and categorical gluing