Internalization of the Groupoid Interpretation of Homotopy Type Theory

Abstract. Homotopical interpretations of Martin-Löf type theory lead toward an interpretation of equality as a richer, more extensional no-tion. Extensional or axiomatic presentations of the theory with princi-ples based on such models do not yet fully benefit from the power of dependent type theory, that is its computational character. Reconciling intensional type theory with this richer notion of equality requires to move to higher-dimensional structures where equality reasoning is ex-plicit. In this paper, we follow this idea and develop an internalization of a groupoid interpretation of Martin-Löf type theory with one universe respecting the invariance by isomorphism principle. Our formal devel-opment relies crucially on ad-hoc polymorphism to overload notions of equality and on a conservative extension of Coq’s universe mechanism with polymorphism.