[Agda] is a proof assistant based on [[Martin-Löf Type Theory|MLTT]] with a countable hierarchy of [[universe polymorphism|explicitly polymorphic]] [[universes]], very powerful [[inductive-inductive types]] and [[inductive-recursive type|inductive-recursive types]], and a flexible [[pattern-matching]] syntax. For a formulation of HoTT in [Agda] see the github repository <https://github.com/HoTT/HoTT-Agda> [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. ### Using [Agda] for Homotopy type theory ### Homotopy type theory has already been [formalized in agda][HoTT-Agda]. You can contribute to it. However, if you want to independently formalizing HoTT in agda, you need to be careful about certain issues with pattern matching. 1. Consider using the latest version of [agda]. Some older versions of agda are known to have bugs when handling absurd patterns. 2. 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. 3. [Agda] does not support higher inductive types (HIT) yet. However, by carefully hiding the constructors of the type and exposing only the induction principle for the type one can simulate it. Some relevant reading material: - The main idea is explained in ["Running circles around in your proof assistant"](http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/). - The [HoTT-Agda] respository has a detailed [README](https://github.com/HoTT/HoTT-Agda/blob/master/lib/types/HIT_README.txt) on how they deal with HITs in agda [hott-agda]: <https://github.com/HoTT/HoTT-Agda> [Agda]: <http://wiki.portal.chalmers.se/agda/pmwiki.php>