El universo de containers se presenta como una construcción particularmente útil para resolver una de las problemáticas claves de la programación genérica: el poder delimitar e inspeccionar el conjunto de tipos de datos con los que habrá de trabajar de forma abstracta. Por otro lado, garantizar la correctitud de los programas es un problema ubicuo en las ciencias de las computación. La forma más segura de hacerlo es dar prueba formal de que el programa cumple con su especificación. Esta tesina presenta una implementación del mencionado universo de containers en el lenguaje Agda, formalizando, a su vez, algunas de sus propiedades.