Agda is a proof assistant based on MLTT? with a countable hierarchy of explicitly polymorphic? universes, very powerful inductive-inductive types? and inductive-recursive types?, and a flexible pattern-matching? syntax.
Agda’s default pattern-matching rules are incompatible with the univalence axiom; they allow one to prove axiom K?. However, there is a flag which restricts them so that they are guaranteed to be expressible in terms of the induction principle without using K. Current versions of Agda use a syntactic check for this, which contains errors, but it has been shown that a modification of the the algorithm yields a correct restriction.
Revision on March 17, 2014 at 08:45:43 by Mike Shulman. See the history of this page for a list of all contributions to it.