Universo est un outil pour Dedukti qui traduit (lorsque c'est possible) un jugement en tant que preuve écrit dans une spécification Cumulative Type System (CTS) en une autre spécification CTS. Les applications possibles sont la minimisation des univers, la rendre des preuves prédictives, et l'interopérabilité entre CTS.