Agda is described as 'dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length' and is an app in the Development category. There are three alternatives to Agda for Linux, Mac, Windows and Online / Web-based. The best alternative is Isabelle, which is both free and Open Source. Other great apps like Agda are F* (Free, Open Source) and Coq (Free, Open Source).
Isabelle is a proof assistant for writing and checking mathematical proofs by computer. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus.
F* is an ML-like functional programming language aimed at program verification. F* can express precise specifications for programs, including functional correctness properties. Programs written in F* can be translated to OCaml or F# for execution.
Coq is a proof assistant, which allows you to write mathematical proofs in a rigorous and formal way, and have them checked for correctness by the computer. It also allows programming with proofs of correctness for the code, and dependent types.