Bibliotecas escritas en Agda

La biblioteca estándar de Agda.

Una biblioteca experimental para Cubical Agda.

Manifestaciones lógicas de conceptos topológicos, y otras cosas. Esta versión adopta el punto de vista univalente.

Compilación de código Agda a Haskell legible.

Formalización Agda de la Introducción a la Teoría de Tipos de Homotopía (por HoTT-Intro).

Combinadores de analizador total en Agda.

Formalización de Lenguajes Regulares en Agda: expresiones regulares, autómatas de estado finito, prueba de equivalencia, prueba del lema de bombeo..

Redacción de tareas universitarias en las que divago sobre clases de tipos y tipos dependientes.

Una plantilla de Agda, configurada para Gitpod (www.gitpod.io) para brindarle entornos de desarrollo efímeros prediseñados en la nube.

Codificación Agda de categorías premonoidales.

El juego de la vida de Conway en Agda..