[Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php) is a proof assistant based on [[MLTT]] with a countable hierarchy of [[universe polymorphism|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](http://people.cs.kuleuven.be/~jesper.cockx/Without-K/) that a modification of the the algorithm yields a correct restriction.