Agda ile yazılmış kütüphaneler

Agda standart kitaplığı.

Cubical Agda için deneysel bir kütüphane.

Topolojik kavramların ve diğer şeylerin mantıksal tezahürleri. Bu sürüm, tek değerli bakış açısını benimser.

Agda kodu okunabilir Haskell'e derleniyor.

Homotopi Tip Teorisine Giriş'in Agda resmileştirilmesi (HoTT-Intro tarafından).

Agda'da Toplam Ayrıştırıcı Birleştiriciler.

Agda'da Düzenli Dillerin Biçimlendirilmesi: düzenli ifadeler, sonlu durum otomatları, eşdeğerlik kanıtı, pompalama lemmasının kanıtı..

Tip sınıfları ve bağımlı tipler hakkında gevezelik ettiğim üniversite ödevi yazısı..

Gitpod (www.gitpod.io) için yapılandırılmış bir Agda şablonu, size bulutta önceden oluşturulmuş, kısa ömürlü geliştirme ortamları sunar.

Premonoidal kategorilerin Agda kodlaması.

Conway'in Agda'daki Hayat Oyunu..