Les travaux de Voevodsky suggèrent une extension de la théorie des types dependents qui résout certains problèmes de modularité (égalité extensionelle et quotients). Un problème est que la justification de cette extension est développée en utilisant le tiers-exclu et l’axiome du choix. Nous présentons un modele de cette extension dans un cadre constructif, et qui peut s’écrire avec avantage directement comme une théorie des types.

Des travaux récents de Christian Sattler (Leeds) montrent comment on peut utiliser ces idées pour décrire une structure de modele similaire a la structure de modele sur les ensembles simpliciaux, mais ou l’on n’utilise jamais le tiers-exclu et l’axiome du choix.