COQ est-il synthétique ou analytique?

Question

Dans le cours Hott de CMU, conférence 1, qui peut être trouvée ici: https://scs.hosted.panopto.com/panopto/pages/viewer.aspx?id=0945cc7f-48b7-4803-81af-e7193a3f461d

À 33:52, Harper donnait une comparaison parallèle entre les théories synthétiques et analytiques, et lorsqu'il a atteint la théorie du PL, il a déclaré que CoQ est analytique et a déclaré que CoQ ne prouve qu'une langue dans sa grammaire mais pas pour l'analyseur lui-même.

J'ai un fort désir d'être en désaccord d'une manière ou d'une autre, mais je n'ai pas une idée claire pourquoi je voudrais faire cela. Je crois que le COQ est très synthétique, il en va de même pour les autres assistants de la preuve basés sur la théorie des types dépendants, car toutes ces langues ne font que construire des programmes. Nous pouvons également exprimer l'algèbre axiomatique dans COQ en utilisant des classes de type par exemple, et concrétiser chaque fois que cela est approprié. Ce modèle est particulièrement le cas dans Agda.

Donc ma question est: Harper était-il non? S'il a raison, quelle partie de mon point de vue provoque mes malentendus?