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.