AgdaAgda is a dependently typed programming language / interactive theorem prover.
agdaThe theory of algebraic graphs formalised in Agda
cubical-1labA formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
cainCategory theory applied to functional programming (undergraduate project)
dicyA builder for LaTeX, knitr, literate Agda, literate Haskell and Pweave that automatically builds dependencies.
msla2014wherein I implement several substructural logics in Agda
org-agda-modeAn Emacs mode for working with Agda code in an Org-mode like fashion, more or less.
ConsHoTTConstructive Interpretations of HoTT
atacaA TACtic library for Agda
agda-modeAccessing Agda's interaction mode via command line & external tactic for Agda.
catA formalization of category theory in cubical Agda
TypeTopologyLogical manifestations of topological concepts, and other things. This version adopts the univalent point of view.
frp agdaFunctional Reactive Programming with Agda
universe-of-syntaxA universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.