Agda je funkčně programovací jazyk závislý na typu.Má induktivní rodiny, tj. Datové typy, které závisí na hodnotách, jako je typ vektorů dané délky.Má také parametrizované moduly, operátory mixfixu, znaky Unicode a interaktivní rozhraní Emacs, které může programátorovi pomoci při psaní programu.Agda je asistentem důkazu.Jedná se o interaktivní systém pro psaní a kontrolu důkazů.Agda je založena na intuitionistické teorii typů, což je základní systém konstruktivní matematiky vyvinutý švédským logikem Per Martin-Löf.Má mnoho podobností s jinými asistenty na základě závislých typů, jako jsou Coq, Epigram, Matita a NuPRL.