No meu projeto explora-se uma fundação alternativa para a matemática baseada nos princípios do construtivismo e na qual a igualdade de objetos matemáticos (tipos) se reduz à observação de que eles têm a mesma estrutura (são isomorfos).