Homotopy Type Theory
Agda (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Agda is a proof assistant based on MLTT?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 May 9, 2014 at 02:20:53 by Alexis Hazell?. See the history of this page for a list of all contributions to it.