I don't have a deep understanding of homotopy type theory, but I'm curious about the difference between coq and HoTT library.

When proving with coq, instead of trying tactics brute force, we roughly guess the tactics to use under a given proposition. Is there any idea in the HoTT library that allows us to consider the direction in which tactics should be used from various forms of propositions?

There is a rough explanation of homotopy type theory, but I couldn't find a rough and direct explanation of how to use the HoTT library. However, I think that the sentence found from https://math.stackexchange.com/a/1159163 may be a hint.

Another thing that HoTT buys you, relative to vanilla type theory, is "proof-irrelevance done right": the "propositions" are the types in which every two elements are equal, so that types built using propositions (like subsets, powersets, quotients, etc.) automatically have the correct equality.

I think this quote says that the form of given proposition need to be approached to the identity type or the type which the proposition belongs.


In coq, when proving a proposition such as A -> B -> A /\ B, if you have an understanding of set theory, you can imagine that you can prove the proposition if A and B can be proved respectively. Therefore, in order to bring the propositions closer to the forms A and B, respectively, we presume to split first.

Similarly, when proving a proposition with HoTT, what kind of understanding do you have to know the form of the proposition you are aiming for and the tactics to guess to get there? If I understand everything in the HoTT book, I can guess such tactics as in set theory, but I would like to hear a "rough explanation" from this perspective.

What I would like to ask is not the part of HoTT that can be used by understanding only set theory, but the manipulation of paths that is used only in homotopy type theory. If we have a rough knowledge of set theory, we can easily see what tactics like the ones in the example are useful for. On the contrary, it is difficult to understand how explanations below affects or helps the proof in the HoTT library.

  • Consider type as space
  • Both space and type have weak ∞-groupoid structure
  • proposition is represented as a path
  • By considering isomorphisms as equivalents, the process of going back and forth between isomorphic structures can be simplified.
  • HIT allows inductive definitions of points and paths in space ... etc.
  • 1
    $\begingroup$ I'm a bit confused about what your actual question is. Are you asking something about a specific library for doing HoTT (in Coq)? Or are you asking what sort of things would be different in Coq vs. something similar based on ideas from HoTT? $\endgroup$
    – Dan Doel
    Oct 10, 2020 at 21:02
  • $\begingroup$ @DanDoel I wanted to ask about the idea of HoTT based on how to use the HoTT library. I may have misunderstood HoTT, so is there anything inappropriate or need to rewrite? $\endgroup$
    – Lageneriq
    Oct 10, 2020 at 22:57
  • 1
    $\begingroup$ I'm having trouble understanding too. Perhaps there is a language issue. Can you give an example of what you mean by "consider the direction in which tactics should be used from various forms of propositions"? $\endgroup$ Oct 12, 2020 at 6:31
  • $\begingroup$ @MikeShulman I edited for a example. $\endgroup$
    – Lageneriq
    Oct 12, 2020 at 12:05
  • $\begingroup$ In that example I would say the answer is "exactly the same". There's nothing intrinsically set-theoretic about logic and its connectives such as conjunction. The encoding of logic is different (in HoTT the "propositions" are defined to be homotopy (-1)-types, whereas in ZFC they are a primitive notion that comes before the sets), but the logic itself behaves essentially the same. $\endgroup$ Oct 13, 2020 at 2:22


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.