Bibliotecas escritas em Agda

A biblioteca padrão Agda.

Uma biblioteca experimental para Cubical Agda.

Manifestações lógicas de conceitos topológicos e outras coisas. Esta versão adota o ponto de vista univalente.

Compilando código Agda para Haskell legível.

Agda formalização da Introdução à Teoria dos Tipos de Homotopia (por HoTT-Intro).

Combinadores totais do analisador em Agda.

Formalização de Linguagens Regulares em Agda: expressões regulares, autômatos de estado finito, prova de equivalência, prova do lema do bombeamento..

Redação de trabalho da faculdade em que divago sobre classes de tipos e tipos dependentes.

Um modelo Agda, configurado para Gitpod (www.gitpod.io) para fornecer ambientes de desenvolvimento efêmeros pré-construídos na nuvem.

Codificação Agda de categorias premonoidais.

O Jogo da Vida de Conway em Agda..