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.
Consider using the latest version of agda. Some older versions of agda are known to have bugs when handling absurd patterns.
You should always use –without-K to compile agda source code. This is because axiom K? is incompatible with univalence axiom. An easy way to ensure this is to use the compiler pragma {-# OPTIONS --without-K #-} at the top of your agda source file.
Agda does not support higher inductive types (yet). However, by carefully hiding the constructors of the type and exposing only the induction principle for the type one can simulate it. See the blog entry titled “Running circles around in your proof assistant” for the exact details on how this can be achieved in agda.