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?

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.

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.

@Ali Caglayan Out of curiosity, does HoTT's axiomization of quotient types break subject reduction, or is that just in Lean?

Higher inductive types are the HoTT generalization of quotients and behave quite well.

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

@Pierre-Marie Pédrot That's why I used the phrasing "Most of" and "to some extent".

- hProps may be propositionally proof-irrelevant but they are not proof-irrelevent. Many proofs still rely on the actual proof content of a hProp, so it is not so different to Prop in some sense.
- You already mentioned that with hProp-resizing you can get impredicativity like with Prop.
- Sure hProp can eliminate into larger universes than Prop can but is that a problem for mimicking Prop?
- Erasure is an interesting point, but I claim that as long as you use hProp like Prop (i.e. no large elim) then you could modify the erasure procedure in some clever way.
- Prop is designed to be compatible with proof-irrelevance but it still needs to be assumed. Are there any developments which explicitly assume otherwise?

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.

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

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.

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.

maybe relevant: https://homotopytypetheory.org/2012/01/22/univalence-versus-extraction/

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.

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.

(And I think that there is already an answer to this problem, which has been advocated in the paper that introduced it. Namely, SProp.)

SProp is the nice subset of hProp and Prop that satisifies both proof-irrelevance *and* erasability by construction.

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.

would SProp even make sense in Lean? For example, I don't think they have plans for erasure/extraction.

Lean has proof-irrelevant Prop

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

@Yannick Forster That is interesting. Do you have an example of a proof that uses the excluded middle in a crucial way?

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?

Maybe, but you need to restrict enough equality in Prop

Typically that means that you must have some variant of the indices-matter flag turned on, and you lose singleton elimination from Prop-equality

What if you use equality in the univalent hierarchy instead?

Yes, but you still need to prevent people from using the Prop equality.

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

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

(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?)

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

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"

So while academic curiosity always led us to finding constructive proofs, excluded middle is important as a safety net

@Yannick Forster What is `CT`

?

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

Ah, Church's Thesis! :)

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)

But yes, indeed, Church's thesis

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?

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.

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 ;-)

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

https://existentialtype.wordpress.com/2012/08/09/churchs-law/

so I meant law as in "law of gravity"

I like the terminology! :)

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"

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

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.

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

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

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: Sep 28 2023 at 11:01 UTC