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
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.