# Code

An important aspect of HoTT is the fact that intensional Martin-Löf type theory has a computational implementation in proof assistants like Coq and Agda.  This forms the basis of Vladimir Voevodsky’s Univalent Foundations program, which uses proof assistants to generate and verify proofs with homotopical content.

### Coq

Collected here are various resources for working (and playing) with HoTT in Coq, mostly hosted at GitHub.  See the resources below for examples, and for instructions on how to set up your own Coq system and GitHub repository so you can get Coqing and share the results.

Main sources:

Tutorials:

Individual repos:

Some individual results:

• Jeremy Avigad’s Coq proof that the higher homotopy groups are abelian, adapted from Dan Licata’s Agda proof. (See Dan’s March 26 blog post.)
• Mike Shulman’s proof that  $\pi^n(S^1)$ is correct. (See Mike’s post.)
• A repository of files for Inductive types in HoTT, by Steve Awodey, Nicola Gambino, and Kristina Sojakova. (See this post.)

### Agda

Another proof assistant is Agda. Agda includes some more advanced features than Coq, but lacks a tactic language; also one must use the option --without-K for consistency with homotopy type theory. Here are some links to Agda code implementing aspects of homotopy type theory.