<p>As far as I understand, in Agda it is possible to represent all of that (i.e. all of Chapter 2 -- there is a library on github which does; AFAIK, the same is true of Coq).  It is only when you get to later chapters that things get dicey.  There are two obvious items:</p>

<ol>
<li>The circle.  This is represented (in Agda) using a <strong>postulate</strong>, and so is not as nice as other things.</li>
<li>$\infty$-groupoids.  But this is an open problem on how to represent infinitely many coherence laws in a finite way.</li>
</ol>

<p>There are other items too, but I have not gotten to reading that part of the Agda formalization yet...  But by and large, most of HoTT can be nicely formalized in both Agda and Coq.</p>

<p>More importantly, both teams of developers are actively working on adapting their systems so that more of HoTT can be handled, at least whenever there is a clear theory of how to implement the needed features.  That has turned out to be challenging in parts.</p>

CC BY-SA 3.0
2014-02-22T13:09:44.513Z
2014-02-22T13:09:44.513Z
Jacques Carette
<p>If you look at <a href="http://books.google.no/books?id=LkDUKMv3yp0C&amp;lpg=PP1&amp;pg=PA296#v=onepage&amp;q&amp;f=false">Notes on Chapter 8</a> you will see what <em>has</em> already been formalized, and I think that's a lot. There are the Coq <a href="https://github.com/HoTT/HoTT">HoTT library</a> and the Agda <a href="https://github.com/HoTT/HoTT-Agda">HoTT-Agda</a> library which formalize large chunks of Homotopy Type Theory.</p>

<p>To get things done in Coq we needed a special version of Coq that was patched just for the purposes of HoTT. However, Coq is moving in the direction of supporting homotopy type theory, so before long we might be able to do it with standard Coq.</p>

<p>In Agda one has to turn on the <code>--without-K</code> option, otherwise Agda thinks all types are 0-types. There are some lingering doubts as to whether <code>--without-K</code> really gets rid of the assumption that everything is a 0-set, or perhaps one could reintroduce it into Agda with tricky uses of pattern matches.</p>

<p>The following aspects of Coq and Agda formalizations are not satisfactory:</p>

<ol>
<li><p>The Univalence axiom is stated as a hypothesis. It would be better if it were built into the system. In particular we would like Coq and Agda to understand the computation rules about the Univalence axiom.</p></li>
<li><p>Likewise, we have to use hacks to get workable higher-inductive types. Again, it would be better to have direct support.</p></li>
</ol>

<p>The trouble with the above deficiencies is that nobody knows how to fix them even in theory. This is an active area of research.</p>

<p>Other than that, I think it's fair to say that HoTT <em>can</em> be mostly done in Coq and Agda, just not in the optimal way.</p>

CC BY-SA 3.0
2014-02-24T09:09:39.623Z
Thanks, is there a good write-up of why univalence and higher inductive types don't sit well with type theories like Agda and Coq?
Martin Berger
CC BY-SA 3.0
2014-02-24T09:11:56.443Z
@MartinBerger this could probably be a separate question (with some definitions for more casual readers, etc).
Artem Kaznatcheev
CC BY-SA 3.0
2014-02-24T09:18:11.083Z
The trouble with univalence and HITs is not that they "don't sit well with type theories like Agda and Coq" but that "we do not know how to do them properly in *any* type theory".
Andrej Bauer
CC BY-SA 3.0
2014-02-24T09:32:26.313Z
@AndrejBauer Univalence and higher inductive types are formaliwsed in the HoTT writeup which is a (semi-formal) type-theory. What is the missing ingredient that prevents a proper formalisation in Agda/Coq? Related, if you are willing to give up Curry-Howard, is there any difficulty formulising univalence and higher inductive types in an LCF-style prover, like Isabelle, using  e.g. LF as a meta-language to formalise proof rules?
Martin Berger
CC BY-SA 3.0
2014-02-24T12:32:06.950Z
What are the computation rules for `ua`, the constant which witnesses the Univalence axiom? What are the computation rules for HITs? We have some ideas, but nothing water-tight.
Andrej Bauer
CC BY-SA 3.0
2014-02-22T15:21:43.720Z
2014-02-24T08:32:54.377Z
2014-02-24T08:32:54.377Z
Andrej Bauer
<p>When we look at <a href="http://homotopytypetheory.org/book/" rel="nofollow noreferrer">the book, Homotopy Type Theory</a> - we see the following topics:</p>

<pre><code>Homotopy type theory 
2.1 Types are higher groupoids
2.2 Functions are functors
2.3 Type families are ﬁbrations
2.4 Homotopies and equivalences
2.5 The higher groupoid structure of type formers
2.6 Cartesian product types
2.7 S-types
2.8 The unit type
2.9 P-types and the function extensionality axiom
2.10 Universes and the univalence axiom
2.11 Identity type
2.12 Coproducts
2.13 Natural numbers
2.14 Example: equality of structures
2.15 Universal properties
</code></pre>

<p>Now <a href="https://cstheory.stackexchange.com/a/14338/608">we know that not all of homotopy type theory is possible is Agda and Coq</a>. </p>

<p>My question is: <strong>What parts of homotopy type theory are not possible in Agda or Coq?</strong></p>

CC BY-SA 3.0
2014-02-22T08:57:12.233Z
Not a particularly well formulated question. What is the relationship between the list of topics and the question?
Dave Clarke
CC BY-SA 4.0
2018-08-23T01:07:10.387Z
@Dave Clarke, The list of topics looks like the context of the mind of the questioner so the answerer knows what the questioner's starting point is and can tailor the answer accordingly. Other learners can also appreciate the answer in the same context and understand that the answer is likely to be useful to them if the answerer is thoughtful and canny regarding human nature. Hope that also helps in other future conversations.
codeshot
<type-systems>
What parts of homotopy type theory are not possible in Agda or Coq?
hawkeye
# What parts of homotopy type theory are not possible in Agda or Coq?

(Asked by: username_0 on 2014-02-22)

When we look at the book, Homotopy Type Theory - we see the following topics:
Homotopy type theory 
2.1 Types are higher groupoids
2.2 Functions are functors
2.3 Type families are ﬁbrations
2.4 Homotopies and equivalences
2.5 The higher groupoid structure of type formers
2.6 Cartesian product types
2.7 S-types
2.8 The unit type
2.9 P-types and the function extensionality axiom
2.10 Universes and the univalence axiom
2.11 Identity type
2.12 Coproducts
2.13 Natural numbers
2.14 Example: equality of structures
2.15 Universal properties

Now we know that not all of homotopy type theory is possible is Agda and Coq. 
My question is: What parts of homotopy type theory are not possible in Agda or Coq?

**Tags:** type-systems
> **Comments:**
> **username_1**: Not a particularly well formulated question. What is the relationship between the list of topics and the question?  
> **username_2**: @Dave Clarke, The list of topics looks like the context of the mind of the questioner so the answerer knows what the questioner's starting point is and can tailor the answer accordingly. Other learners can also appreciate the answer in the same context and understand that the answer is likely to be useful to them if the answerer is thoughtful and canny regarding human nature. Hope that also helps in other future conversations.  

---

## 2 answers

### Answer by username_4 on 2014-02-22. Score: 21 | Accepted answer

If you look at [Notes on Chapter 8](http://books.google.no/books?id=LkDUKMv3yp0C&lpg=PP1&pg=PA296#v=onepage&q&f=false) you will see what *has* already been formalized, and I think that's a lot. There are the Coq [HoTT library](https://github.com/HoTT/HoTT) and the Agda [HoTT-Agda](https://github.com/HoTT/HoTT-Agda) library which formalize large chunks of Homotopy Type Theory.

To get things done in Coq we needed a special version of Coq that was patched just for the purposes of HoTT. However, Coq is moving in the direction of supporting homotopy type theory, so before long we might be able to do it with standard Coq.

In Agda one has to turn on the `--without-K` option, otherwise Agda thinks all types are 0-types. There are some lingering doubts as to whether `--without-K` really gets rid of the assumption that everything is a 0-set, or perhaps one could reintroduce it into Agda with tricky uses of pattern matches.

The following aspects of Coq and Agda formalizations are not satisfactory:

1. The Univalence axiom is stated as a hypothesis. It would be better if it were built into the system. In particular we would like Coq and Agda to understand the computation rules about the Univalence axiom.
2. Likewise, we have to use hacks to get workable higher-inductive types. Again, it would be better to have direct support.

The trouble with the above deficiencies is that nobody knows how to fix them even in theory. This is an active area of research.

Other than that, I think it's fair to say that HoTT *can* be mostly done in Coq and Agda, just not in the optimal way.

> **Comments:**
> **username_5**: Thanks, is there a good write-up of why univalence and higher inductive types don't sit well with type theories like Agda and Coq?  
> **username_6**: @MartinBerger this could probably be a separate question (with some definitions for more casual readers, etc).  
> **username_4**: The trouble with univalence and HITs is not that they "don't sit well with type theories like Agda and Coq" but that "we do not know how to do them properly in *any* type theory".  
> **username_5**: @AndrejBauer Univalence and higher inductive types are formaliwsed in the HoTT writeup which is a (semi-formal) type-theory. What is the missing ingredient that prevents a proper formalisation in Agda/Coq? Related, if you are willing to give up Curry-Howard, is there any difficulty formulising univalence and higher inductive types in an LCF-style prover, like Isabelle, using  e.g. LF as a meta-language to formalise proof rules?  
> **username_4**: What are the computation rules for `ua`, the constant which witnesses the Univalence axiom? What are the computation rules for HITs? We have some ideas, but nothing water-tight.  

---

### Answer by username_3 on 2014-02-22. Score: 12

As far as I understand, in Agda it is possible to represent all of that (i.e. all of Chapter 2 -- there is a library on github which does; AFAIK, the same is true of Coq). It is only when you get to later chapters that things get dicey. There are two obvious items:

1. The circle. This is represented (in Agda) using a **postulate**, and so is not as nice as other things.
2. $\infty$-groupoids. But this is an open problem on how to represent infinitely many coherence laws in a finite way.

There are other items too, but I have not gotten to reading that part of the Agda formalization yet... But by and large, most of HoTT can be nicely formalized in both Agda and Coq.

More importantly, both teams of developers are actively working on adapting their systems so that more of HoTT can be handled, at least whenever there is a clear theory of how to implement the needed features. That has turned out to be challenging in parts.


---

