[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. Homotopy type theory has already been formalized in agda [HoTT-Agda] repository. You can contribute to it. ### Using [Agda] for Homotopy type theory ### In case you want to independently formalizing HoTT in agda, you need to be careful about certain issues. 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. An easy way to ensure this is to use the compiler pragma `{-# OPTIONS --without-K #-}` at the top of your agda source file. What is wrong with axiom K? One of the key ideas of Homotopy type theory is to regard the identity `Id x y` as the path between the points `x` and `y`. [[Axiom K]] allows one to prove uniqueness of elements in the identity type which essentially means that non-trivial topological spaces like the loop will be contracted to a point. For details see the post on [Identity Elimination]. 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. update: there is now `{-# OPTIONS --cubical #-}` and HITs 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/). - See the [HoTT-Agda] respository [README](https://github.com/HoTT/HoTT-Agda/#inductive-types-and-higher-ones) 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> [Identity Elimination]: <http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/> category: proof assistants