Patrick Nicodemus (Nov 28 2021 at 17:45): Patrick Nicodemus (Nov 28 2021 at 17:45):Are there any disadvantages to using HoTT rather than vanilla Coq to write proofs? If you are not doing synthetic homotopy theory but ordinary mathematics, are there reasons to prefer one over the other?
I think that what HoTT calls "path induction" is more or less just the usual induction axiom for equality in a dependent type theory, so I am not sure reasoning about dependent equality would be any easier in vanilla Coq. What benefits are there to using the built in Coq options for "Set" and "Prop" vs homotopy type theory which works entirely in "Type" with custom "hProp" and "hSet"
To specify, I am interested in proving theorems about the category of simplicial sets and the simplex category.
Here is a more specific question: for various automation tools and solvers - auto, coq-hammer, - will these be more effective in vanilla coq vs homotopy type theory?
Ali Caglayan (Nov 28 2021 at 22:40):By HoTT I mean intentional Martin-Löf type theory together with the univalence axiom and higher inductive types (HITs). Let's compare HoTT and "vanilla" Coq. Coq's underlying type theory can be thought of as intentional Martin-Löf type theory together with uniqueness of identity proofs (UIP). This is not really true, but is fine for our comparison.
Without UIP, there are models of intentional MLTT which do not satisfy UIP. The first such model is the groupoid model by Hoffman and Streicher. There types can be interpreted as (1-)groupoids, so that the identity type between terms of types do not have a unique element. HoTT takes this idea all the way up and says types should be thought as oo-groupoids (i.e. simplicial sets). The homs of 1-groupoids are sets (i.e. types with UIP). The homs of oo-groupoids are again oo-groupoids.
Are there any disadvantages to using HoTT rather than vanilla Coq to write proofs? If you are not doing synthetic homotopy theory but ordinary mathematics, are there reasons to prefer one over the other?
I think for formalizing "ordinary" mathematics, (almost) vanilla Coq is better suited.
I think that what HoTT calls "path induction" is more or less just the usual induction axiom for equality in a dependent type theory, so I am not sure reasoning about dependent equality would be any easier in vanilla Coq.
Yep, this is exactly the same.
What benefits are there to using the built in Coq options for "Set" and "Prop" vs homotopy type theory which works entirely in "Type" with custom "hProp" and "hSet"
Coq also uses "Type" though not as frequently. Universe polymorphism is still somewhat experimental. Much of Coq's formalization using "Prop" can be mimicked to some extent with "hProp" but there is no inherit benefit to doing so.
To specify, I am interested in proving theorems about the category of simplicial sets and the simplex category.
If you are interested in formalizing regular mathematics then vanilla Coq is better suited. You can do almost everything you normally do with sets. There are some nuances when it comes to quotients for which there are (at least) two solutions. You can use Coq's setoid machinery or you can axiomatize a quotient type (like lean does). The latter happens to be an idea that HoTT uses.
So the question is, why on earth do people bother with HoTT then?
In short there are two main schools of thought when it comes to this, with a lot of overlap. The first is that the univalence axiom is inherently correct and should be used to formalize normal mathematics, this can be thought of as the "Unimath point of view". There is a large effort to formalize undergraduate mathematics using the univalence axiom.
The second point of view is that, when you do definitions/lemmas/theorems about HoTT you are really proving things about simplicial sets (and every Grothendieck oo-topose generalization thereof). This is why we can do synthetic homotopy theory in HoTT, we can play around with types just like you can play around with oo-groupoids in homotopy theory.
So coming back to what you want to do. I would personally pick a category theory library for Coq (there are a few out there). Just like it is done on paper you would formalize modal categories and show that simplicial sets (as a presheaf category on the simplex category) has a model structure and play around with that.
HoTT gives you a language for reasoning inside that (oo-)category, but not about the (oo-)category itself. It is a wide open problem if infinitely-coherent structures can be expressed within HoTT (though there are extensions which allow this somewhat). This is analogous to how working in ZFC doesn't really tell you much about the ambient category of sets, you still have to develop the theory etc.
Sorry this answer dragged on a bit, but feel free to ask about any of it.
Patrick Nicodemus (Nov 28 2021 at 23:37):Thank you for this helpful answer. I don't have follow up questions right now because there's a lot of information out there I have to digest and make sense of, but I understand the gist of what you're saying and it makes sense to me.
Joshua Grosso (Nov 29 2021 at 04:21):@Ali Caglayan Out of curiosity, does HoTT's axiomization of quotient types break subject reduction, or is that just in Lean?
Li-yao (Nov 29 2021 at 04:52):Higher inductive types are the HoTT generalization of quotients and behave quite well.
Pierre-Marie Pédrot (Nov 29 2021 at 07:32):Much of Coq's formalization using "Prop" can be mimicked to some extent with "hProp"
I quite don't agree on this claim. Axiom-free Coq Prop vs. HoTT hProp are very different beasts. By definition, the latter is made of propositionally proof-irrelevant types (and you can make it impredicative assuming you have resizing rules). Meanwhile, vanilla Prop is not even proof-irrelevant. It's designed to be compatible with it, but without further assuming proof-irrelevance you actually have to treat it relevantly in proofs. Rather, Prop is a hodgepodge of features stacked together on one single sort. It's impredicative, has no large elimination (large as in universe level, not homotopy level) and is erased by extraction. None of these properties are shared by hProp. So as you see you can't use hProp to perform any of those tasks...
Ali Caglayan (Nov 29 2021 at 08:12):@Pierre-Marie Pédrot That's why I used the phrasing "Most of" and "to some extent".
I am failing to see how any of these give Prop properties hProp cannot mimic? Of course the converse direction is completely out of the question, I don't at all claim every hPropy proof can become one with Prop.
Pierre-Marie Pédrot (Nov 29 2021 at 08:14):Sure hProp can eliminate into larger universes than Prop can but is that a problem for mimicking Prop?
Well, then you get unique choice which is a big no-no for erasure. There are very simple hProps that are not erasable (e.g. singletons).
Ali Caglayan (Nov 29 2021 at 08:25):Joshua Grosso said:
Ali Caglayan Out of curiosity, does HoTT's axiomization of quotient types break subject reduction, or is that just in Lean?
No subject-reduction is not broken with quotients. The path constructor is postulated as an term of the identity type. IIRC lean went a bit further and made this a definitional equality instead, which I've heard can cause problems. I haven't seen a concrete example of this though. I think @Pierre-Marie Pédrot knows one.
Ali Caglayan (Nov 29 2021 at 08:28):Pierre-Marie Pédrot said:
Well, then you get unique choice which is a big no-no for erasure. There are very simple hProps that are not erasable (e.g. singletons).
Then just don't eliminate into larger universes 0:-). If you are using a singleton hProp, as long as you don't do anything you cannot do with coq's True, I don't see the problem for erasure.
Karl Palmskog (Nov 29 2021 at 08:53):maybe relevant: https://homotopytypetheory.org/2012/01/22/univalence-versus-extraction/
Pierre-Marie Pédrot (Nov 29 2021 at 09:05):If you are using a singleton hProp, as long as you don't do anything you cannot do with coq's True
By singleton I mean the type Σy : A. x = y. You will never be able to erase this type whatsoever. And nonetheless there is no way to enforce that you depend on this in a non-computational way. Claiming otherwise is like saying that you can always write MLTT inside LISP.
Pierre-Marie Pédrot (Nov 29 2021 at 09:06):In this view, the conclusion of the blog post looks wrong to me. hProp enjoys unique choice by construction and unique choice smashes aways erasability.
Pierre-Marie Pédrot (Nov 29 2021 at 09:08):(And I think that there is already an answer to this problem, which has been advocated in the paper that introduced it. Namely, SProp.)
Pierre-Marie Pédrot (Nov 29 2021 at 09:08):SProp is the nice subset of hProp and Prop that satisifies both proof-irrelevance and erasability by construction.
Paolo Giarrusso (Nov 29 2021 at 09:36):https://homotopytypetheory.org/2013/10/28/the-truncation-map-_-ℕ-‖ℕ‖-is-nearly-invertible/ is a further fun fact relevant to erasability, tho Pierre-Marie's example is simpler.
Karl Palmskog (Nov 29 2021 at 11:15):would SProp even make sense in Lean? For example, I don't think they have plans for erasure/extraction.
Gaëtan Gilbert (Nov 29 2021 at 11:19):Lean has proof-irrelevant Prop
Yannick Forster (Dec 01 2021 at 13:26):Even independent of erasure there can be drawbacks when unique choice is provable. (this answer is kind of an advertisement for my and my collaborators' work) First, when doing constructive reverse mathematics one becomes blind wrt unique choice, meaning in HoTT you can't prove that a nice theorem relying on unique choice is actually equivalent to it (I'm not aware of any such theorem, but in principle that's still true). And secondly, when doing synthetic computability theory or synthetic undecidability proofs like in our Coq library of undecidability proofs not having unique choice is crucial because it allows to do proofs using excluded middle in a sound way - I doubt that there ever can be machine-checked advanced computability theory in HoTT
Arthur Azevedo de Amorim (Dec 01 2021 at 14:30):@Yannick Forster That is interesting. Do you have an example of a proof that uses the excluded middle in a crucial way?
Meven Lennon-Bertrand (Dec 01 2021 at 14:41):Couldn’t you in priciple use Prop without unique choice such as Coq’s along with a hierarchy of univalent types, so that you could use univalence in the relevant world without having the unique choice you care about not having?
Pierre-Marie Pédrot (Dec 01 2021 at 14:42):Maybe, but you need to restrict enough equality in Prop
Pierre-Marie Pédrot (Dec 01 2021 at 14:42):Typically that means that you must have some variant of the indices-matter flag turned on, and you lose singleton elimination from Prop-equality
Meven Lennon-Bertrand (Dec 01 2021 at 14:47):What if you use equality in the univalent hierarchy instead?
Pierre-Marie Pédrot (Dec 01 2021 at 14:48):Yes, but you still need to prevent people from using the Prop equality.
Yannick Forster (Dec 01 2021 at 15:07):Arthur Azevedo de Amorim said:
Yannick Forster That is interesting. Do you have an example of a proof that uses the excluded middle in a crucial way?
If you're willing to take "If the complement of p many-one reduces to the complement of q, then p many-one reduces to q" as an example, then yes. But it's kind of a boring example, and I don't have an interesting example of a proof relying on excluded middle yet :) In the end we were always able to constructivise proofs, but often with nontrivial work. I have three anecdotes / ideas how to get an example: First, if I remember correctly, the undecidability proof of semiunification simplified and formalised by @Andrej Dudenhefner did rely on excluded middle at some point, but Andrej was able to get rid of it. Secondly, in the work on Kolmogorov complexity by Nils Lauermann with @Fabian Kunze an intermediate step crucially relied on excluded middle (that is: the wanted theorem was fully proved, but relied on excluded middle). Only as a second step the proof was changed to only rely on Markov's principle, and we're currently analysing whether even this is necessary. The factorisation into "finding a proof based on logical axioms" and "getting rid of the axioms" is crucial I think. One could still assume an inconsistent excluded middle axiom and then get rid of it in a second step, but from the point of motivation this might be difficult. And thirdly, with Niklas Mück and @Dominik Kirst we're currently working on the arithmetical hierarchy and Post's theorem. Given that textbook proofs there talk about prenex normal form a lot, I'd be surprised if no axiom stronger than MP and possibly even as strong as excluded middle would be necessary
Arthur Azevedo de Amorim (Dec 01 2021 at 15:39):@Yannick Forster I see... I indeed tried grepping for instances of classical in your sources but couldn't find any!
The point about being able to start with a classical proof and only later try to remove those axioms makes a lot of sense. But if the end product is supposed to be free of axioms, does it matter that much if you are working with or without HoTT?
Arthur Azevedo de Amorim (Dec 01 2021 at 15:42):(Also, isn't the excluded middle for hProp consistent? I guess it would break the adequacy of the synthetic encoding, but it wouldn't hurt logical consistency, right?)
Yannick Forster (Dec 01 2021 at 15:53):You can prove LEM -> AUC -> forall p, decidable p (with decidable p being a resonable proposition saying the right thing, LEM being the law of excluded middle and AUC being the axiom of unique choice). So yes, logical consistency is not hurt, you just can't do classical synthetic undecidability proofs anymore. For the work on more general synthetic computability theory, we also assume the axiom CT, and we have that CT -> exists p, ~ decidable p, so in this context assuming LEM and AUC is inconsistent
Yannick Forster (Dec 01 2021 at 15:55):And it's not always clear that you can get rid of LEM, we had to work hard in many cases. It's one thing to start a big project and saying "I'll assume LEM for now and will try to get rid of it later, but if that doesn't work my result is still interesting" but a totally different thing to say "I'll assume LEM for now and will try to get rid of it later, but if that doesn't work my whole project is doomed"
Yannick Forster (Dec 01 2021 at 15:56):So while academic curiosity always led us to finding constructive proofs, excluded middle is important as a safety net
Arthur Azevedo de Amorim (Dec 01 2021 at 16:04):@Yannick Forster What is CT?
Yannick Forster (Dec 01 2021 at 16:10):An axiom in constructive mathematics stating that for every function f : nat -> nat there exists a Turing machine computing it . I have a summary of what that means in Coq here. It allows doing computability theory synthetically, without actually considering models of computation, which is great, because the thing that hinders machine-checked computability is that encoding programs in models of computations is a pain
Arthur Azevedo de Amorim (Dec 01 2021 at 16:13):Ah, Church's Thesis! :)
Yannick Forster (Dec 01 2021 at 16:16):I've met many people (including myself) who have been confused by the spelled out name when encountering it, so I usually avoid that :) (plus the wikipedia article makes a tremendously bad job explaining why it's a good name in the end)
Yannick Forster (Dec 01 2021 at 16:16):But yes, indeed, Church's thesis
Karl Palmskog (Dec 01 2021 at 16:37):this [calling a formula CT] goes against the usual interpretation of "Church's thesis" as "Church's law", i.e., an empirical claim (about existence of methods of computation in the actual world). Can you say why it's a good name?
Yannick Forster (Dec 01 2021 at 16:58):Now it becomes funny: Church's law is yet again a technical term in constructive mathematics, different but related to CT, and you might find it even more confusing :) I can try to give you intuition: Lets call the statement "Every intuitively calculable function is computable" (for some common def. of "computable") the "Church Turing thesis". Now this informal belief is used a lot in textbooks on computability to shorten proofs: Instead of spelling out a program in the chosen model of computation the author just argues a bit, then says "Now by the Church Turing thesis, we obtain a program and that's enough, Qed". In machine-checked proofs, this won't work: You can't just handwave intuitive computability away. But, in machine-checked proofs in systems based on constructive logic, and even more so in systems like Coq where very function _is_ a program, you can assume the axiom CT and then replace every informal textbook use of the Church Turing thesis by a formal use of the CT axiom.
Dominik Kirst (Dec 01 2021 at 17:01):Arthur Azevedo de Amorim said:
Yannick Forster That is interesting. Do you have an example of a proof that uses the excluded middle in a crucial way?
One example where we couldn't eliminate the usage of LEM (yet) is the undecidability of the classical deduction system for ZF set theory. As part of the proof you need to extract a solution to an undecidable problem from a ZF-deduction of a formula encoding such a solution. With LEM this is easy since then the deduction system is sound for some standard model directly yielding the actual solution. Without LEM we are currently not even sure the formula has the right structure to allow this extraction constructively, so we might have to reformulate the encoding and even then it would be quite some work left to avoid LEM. So even though this is not an example where LEM is strictly required, it is an example where Yannick's "I'll assume LEM for now and will try to get rid of it later, but if that doesn't work my result is still interesting" slogan fits ;-)
Yannick Forster (Dec 01 2021 at 17:01):Oops, I was wrong about Church's law. I was thinking about Church's rule, which is the term used, Church's law is not used in constructive mathematics I think
Karl Palmskog (Dec 01 2021 at 17:05):https://existentialtype.wordpress.com/2012/08/09/churchs-law/
Karl Palmskog (Dec 01 2021 at 17:06):so I meant law as in "law of gravity"
Yannick Forster (Dec 01 2021 at 17:10):I like the terminology! :)
Karl Palmskog (Dec 01 2021 at 17:15):OK, so one interpretation using Bob's reasoning is that your CT is actually "Church's law inside (p)C(U)IC", while I would normally think of CT without qualification as "Church's law as applied to the empirical world"
Patrick Nicodemus (Dec 01 2021 at 18:52):@Ali Caglayan could you elaborate on what you mean when you suggest that Coq is "like" or has something analogous to UIP? I understand that you are not literally saying Coq has UIP, but it seems to me you are suggesting that there is some kind of spectrum between MLTT and MLTT+ UIP/Axiom K and Coq lies between them. What do you mean by this?
Patrick Nicodemus (Dec 01 2021 at 18:54):And Yannick, my experience is that computability theory relies on excluded middle extremely heavily, although I'm not sure what you mean by 'synthetic computability' here.
Paolo Giarrusso (Dec 01 2021 at 20:10):@Patrick Nicodemus “synthetic computability” means that computable functions are a primitive of the system, namely, Gallina functions — as opposed to (analytic?) computability where you define computable functions by formalizing Turing machines or what have you.
Yannick Forster (Dec 02 2021 at 07:49):What Paolo says, yes :point_up: @Patrick Nicodemus It really depends what you mean by "relies" here. Do books on computability theory use excluded middle (and even the axiom of choice) heavily? Yes, definitely. But can the theorems really only be proved assuming excluded middle and are they unprovable without? We don't know. In our experience, all results we proved did not rely on excluded middle in the end, nor on any other axiom (apart from Markov's Principle in maybe 2 cases). And I just want to mention that the difference between analytic and synthetic computability is interesting to mache machine-checked computability feasible, but not relevant for the question whether a theorem needs classical logic or not
Ali Caglayan (Dec 02 2021 at 12:41):Patrick Nicodemus said:
Ali Caglayan could you elaborate on what you mean when you suggest that Coq is "like" or has something analogous to UIP? I understand that you are not literally saying Coq has UIP, but it seems to me you are suggesting that there is some kind of spectrum between MLTT and MLTT+ UIP/Axiom K and Coq lies between them. What do you mean by this?
I didn't mean anything deeper by this. Coq is not literally implementing MLTT+UIP. But Coq does have Prop, which eq lives in and doesn't satisfy UIP by default, that has to be assumed.
Last updated: Apr 19 2024 at 07:02 UTC