Homotopy Type Theory Agda > history (Rev #6, changes)

Showing changes from revision #5 to #6: Added | Removed | Changed

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. For a formulation of HoTT inAgda see the github repository https://github.com/HoTT/HoTT-Agda

AgdaHomotopy type theory has already been formalized in agda ‘s default pattern-matching rules are incompatible with the HoTT-Agdaunivalence axiom repository. You can contribute to it.; 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.

Using Agda for Homotopy type theory

Homotopy In type case theory you has want already to been independently formalizing HoTT in agda, you need to be careful about certain issues.formalized in 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 An easy way to ensure this is because to use the compiler pragmaaxiom K?{-# OPTIONS --without-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.

   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.

   Some relevant reading material:

   • The main idea is explained in “Running circles around in your proof assistant”.

   • The HoTT-Agda respository has a detailed README on how they deal with HITs in agda