Agda (Rev #2, changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

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.