17
$\begingroup$

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 fibrations
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?

Improve this question
$\endgroup$
2
  • 4
    $\begingroup$ Not a particularly well formulated question. What is the relationship between the list of topics and the question? $\endgroup$
    – Dave Clarke
    Commented Feb 22, 2014 at 8:57
  • $\begingroup$ @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. $\endgroup$
    – codeshot
    Commented Aug 23, 2018 at 1:07

2 Answers 2

Reset to default
21
$\begingroup$

If you look at Notes on Chapter 8 you will see what has already been formalized, and I think that's a lot. There are the Coq HoTT library and the Agda 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.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ 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? $\endgroup$
    – Martin Berger
    Commented Feb 24, 2014 at 9:09
  • 1
    $\begingroup$ @MartinBerger this could probably be a separate question (with some definitions for more casual readers, etc). $\endgroup$
    – Artem Kaznatcheev ♦
    Commented Feb 24, 2014 at 9:11
  • 4
    $\begingroup$ 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". $\endgroup$
    – Andrej Bauer
    Commented Feb 24, 2014 at 9:18
  • 1
    $\begingroup$ @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? $\endgroup$
    – Martin Berger
    Commented Feb 24, 2014 at 9:32
  • 5
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Feb 24, 2014 at 12:32
12
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.