Projet de recherche en informatique théorique visant à simplifier et automatiser l'élimination de l'univalence dans les systèmes de types. Il permet de transformer des preuves complexes en calculs plus simples et plus efficaces, facilitant ainsi le développement de logiciels formellement vérifiés. Basé sur des concepts avancés de théorie des types, il s'adresse principalement aux chercheurs et développeurs en informatique fondamentale.