Agda is another proof assistant which is based on the logical framework formulation of intuitionistic type theory, but adds numerous features inspired by practical programming languages (Norell 2008). It is an intensional theory with decidable judgments and a type-checker similar to Coq’s. However, in contrast to Coq it is based on Martin-Löf’s predicative intuitionistic type theory.