哥德堡的证明编辑传统
Agda的早期实现属于查尔摩斯理工大学和哥德堡大学的类型论研究。卡塔里娜·科康以Haskell编写原系统；它承接哥德堡既有证明辅助工具的工作，把构造和检查证明与程序放在相近的语言框架内。项目后来的沿革将这一版本称为Agda 1，以便同重新实现的Agda区分。
1999年，卡塔里娜·科康与蒂埃里·科康在巴黎LFM会议论文《结构化类型论》中介绍已经实现的Agda。论文开篇明确说它只说明实际系统的一部分：研究重点是依赖函数类型、局部定义与包机制，记录类型、数据类型和情况表达式虽已实现，却未在该文展开。1999年因而是可核实的公开技术说明年份，不宜径称软件首次下载日。
检查证明项，而非只执行命令
在这种系统中，类型可以表达待证明的命题，证明则以具有该类型的项给出。使用者编辑这些项，系统检查它们是否符合所声明的类型。科康2005年课程讲义强调直接操作证明项，区别于用一串策略命令改变内部证明状态的方式。
以命题“A蕴含A”为例，讲义给出的证明接收一个A类型的输入，再把它本身返回。把A也作为参数，便得到适用于不同类型的恒等函数。这一小例子同时表现为一个程序和一个逻辑证明：函数体的构造必须同其声明相符，而不是先输出一句“命题成立”再补理由。
参考：[3]
让尚未完成的构造可继续编辑
1999年论文允许在表达式中暂留问号，每个问号表示一个尚未确定的元变量。系统可以保存关于这些空位的约束，使使用者逐步补全表达式；未完成的项并不会因有空位就自动成为完整证明。局部定义可将重复使用的构造命名，包则把共享一组参数的定义放在一起。
这种组织方法同交互界面相配合。托马斯·哈尔格伦为Agda开发图形界面Alfa，文本用户则可通过Emacs界面工作。2004年开发报告说，两种界面都连接同一以Haskell编写的系统；Emacs界面用文本协议通信。当时报告将实现规模记为约一万五千行，所描述的是当时版本的状况。
稳定版本、试验功能与合作
科康在2004年11月报告中说明，已有使用一年多的稳定版本，也能下载较新的不稳定版本。试验方向包括隐藏参数、带类机制的重载，以及字符、字符串和整数等内建类型。这提供了实际分发状态的同期记录，同时也提醒读者区分稳定功能与正在试验的扩展。
报告还记述同日本产业技术综合研究所开始合作，工作包括改善文档和接入其他自动证明工具。后来的项目沿革将这项合作置于2004年，并记载瑞典与日本之间的实现者会议。早期Agda因此既是类型论实现，也是由界面、文档、例子和研究交流维持的工具。
2007年论文属于新的实现阶段
2005年课程讲义已经用数据类型、情况表达式、记录和模块解释Agda，并以数个小程序说明如何在系统中构造证明。它还介绍类型检查与终止性检查，说明可执行的表达式要受系统规则约束。使用者仍须清楚声明、定义和假设各自承担什么作用。
乌尔夫·诺雷尔2007年博士论文第97页则把其Agda称为旧语言的重新设计和重新实现，并说明该章讲的是可下载的2.1.0版。这一阶段不应覆盖此前版本的存在。早期Agda的历史由1999年的实现说明、2004年的分发报告和2005年的课程材料连起来；后续重写延续其名称和研究传统，同时形成新的设计。