Los sistemas de tipos desempeñan un papel esencial en la garantía del comportamiento adecuado de los programas. Sin embargo, estos imponen cierta rigidez a la hora de escribir dichos programas, ya que se deben adherir estrictamente a las reglas de tipado establecidas. Existen una serie de “sistemas módulo isomorfismos” [DD19; DD23; AD20; DM15; Sot20; SDM20] que proponen flexibilizar esta restricción considerando aquellos tipos que sean isomorfos como idénticos. En simples palabras, dos tipos se consideran isomorfos cuando es posible convertir uno en el otro, y viceversa, sin perder información en el proceso. Es decir, si dos tipos A y B son isomorfos, es posible usar un término de tipo A en cualquier lugar que se espere un término de tipo B aplicando la conversión correspondiente. Trabajar con tipos isomorfos provee mayor flexibilidad en la construcción de programas y permite combinarlos de formas que normalmente no serían posibles.
Este trabajo se centra principalmente en el primero de estos sistemas, llamado Sistema I. Aquí, se presenta una formalización de una adaptación de dicho sistema en el lenguaje Agda, además, se añade el tipo Top y los isomorfismos correspondientes para ampliar aún más la flexibilidad del sistema. Esta formalización va acompañada de pruebas formales que demuestran el cumplimiento de diversas propiedades, siendo la normalización fuerte una de las más cruciales. Es importante destacar que la prueba de normalización fuerte utiliza la técnica de logical relations pero con predicados distintos a los presentados en la prueba de candidatos de reducibilidad de Girard.