Sistema I es un lambda cálculo simplemente tipado con pares, extendido con una teoría ecuacional obtenida a partir de los isomorfismos de tipos existentes entre los tipos simples con pares. En este trabajo en progreso proponemos una extensión de Sistema I hacia tipos polimórficos, añadiendo al sistema de tipos tanto el cuantificador universal como sus isomorfismos relacionados.