From a homotopical perspective, Coq’s built-in sort `Prop` is like an undecided voter, wooed by both the extensional and the intensional parties. Sometimes it leans one way, sometimes the other, at times flirting with inconsistency.

In the traditional view of Coq, we think of types in `Prop` as *propositions* and their inhabitants as *proofs*. Thus, knowing *that* a type of sort `Prop` is inhabited is considered more important than knowing anything *about* a particular inhabitant of it. This point of view is officially enshrined in Coq’s mechanism for “extraction” to executable code (such as ML or Haskell), which purposely discards all information about inhabitants of types in `Prop`. (Something like this is important for developing verified computer software in Coq — we don’t want the resulting software to have to carry along the baggage of the proofs that it is correct.)

In homotopy type theory, it’s natural to want to interpret this by thinking of `Prop` as a universe of h-propositions (types of h-level 1, which are contractible as soon as they are inhabited). But for better or for worse, this is an invalid way to think — at least, given the way Coq currently treats `Prop`. For one thing, nowhere *inside* the Coq type system is the “proof-irrevelance” of `Prop` enforced: it appears perfectly consistent for a type in `Prop` to have multiple distinct inhabitants. In particular, nothing forces Coq’s built-in `Prop`-valued identity types “`eq`” to be extensional (other than an axiom to that effect).

But actually, things are even worse than that: as soon as there are types anywhere in Coq that are not h-sets, then there must be types in `Prop` that are not h-props. Specifically, the `Prop`-valued equality of any type is provably equivalent, in Coq, to its `Type`-valued equality (i.e. its path type) — thus the `Prop`-valued equality of a non-hset must be a non-hprop.

Why must the two equalities be equivalent? The short answer is that they have the same inductive definition, hence the same universal property. But something has to be said about why that is, since in general an inductive type in sort `Prop` *doesn’t* have the same universal property as the corresponding one in sort `Type`. And the reason for *that* goes back to thinking of `Prop` as consisting of h-propositions again (see what I mean about being undecided?).

Specifically, if `Prop` were to consist of h-props, then we would then have to regard inductively defined types in sort `Prop` (which include propositional operations like “and”, “or”, and “there exists”, and also the equality `eq`) as being obtained from ordinary inductive types (in sort `Type`) by applying the h-prop reflection (= bracket type, squash type, support, `is_inhab`, etc.). In particular, the `Prop`-valued equality `eq` would be the h-prop reflection of the path type (and in particular would be an h-prop). And if inductive types in `Prop` were defined in this way, we would only be able to eliminate out of them into other types in `Prop` (by combining the eliminator of the original inductive type with the universal property of the h-prop reflection). Reflective subcategories are like one-way driveways: once you’ve been reflected into h-prop, you can’t back up without suffering Severe Tire Damage.

And, indeed, Coq does *mostly* adhere to this philosophy in its treatment of `Prop`: the eliminators for inductively defined types in `Prop` can generally only be applied when the target is also of sort `Prop`. However, Coq also includes a sneaky back alley leading out of `Prop`: singleton elimination. If an inductive type in sort `Prop` has at most one constructor and all arguments of that constructor are in `Prop`, then Coq allows us to eliminate out of it into all types, not just those in `Prop`. One argues, I guess, that in this case, the singleton constructor is “uninformative” and so it causes no harm to eliminate out of it.

In particular, since equality/identity types can be defined as an inductive family using only one constructor which takes no arguments, this rule applies to them. Hence, Coq’s `Prop`-valued equality has exactly the same universal property as the `Type`-valued path-types, and so they are equivalent.

(It’s a tiny bit tricky to prove this in Coq, though, since the induction principles that Coq builds for inductive types of sort `Prop` are hamstrung compared to those for ordinary inductive types: they don’t allow for dependency of the target on the inductive type itself. This is, again, in keeping with the “proof-irrelevance” philosophy; nothing can depend interestingly on an inhabitant of a proposition. However, Coq’s induction principles like `eq_rect` are not basic but are implemented in terms of `match` syntax, and the latter still allows full dependent elimination even for inductive types in `Prop`. We can tell Coq to build us a better induction principle for `eq` by saying `Scheme eq_ind' := Induction for eq Sort Prop.`, and then use it with `induction p using eq_ind'`.)

It follows that if we add to Coq an axiom which contradicts extensionality (such as univalence), then while the type system need not become inconsistent (since, as I said, nowhere *internally* does Coq enforce proof-irrelevance for `Prop`), the *extraction process* (which does assume proof-irrelevance) becomes inconsistent. What I mean by that is, assuming univalence (and nothing else), we can define a term inside of Coq which *extracts to* a term claiming to inhabit the empty type.

How does this work? First consider a simpler claim: we can define a term `X : bool` and prove in Coq that `X = true`, yet observe that `X` extracts to `false`. To define such an `X`, consider the automorphism `not : bool -> bool`. It’s easy to prove that this is an equivalence, so by univalence, it induces a path from `bool` to itself (as a term of type `Type`). Since path-types are equivalent to eq-types, this induces an inhabitant of Coq’s `Prop`-valued equality `bool = bool`. Now, eliminate along this equality to transport `false : bool` into a new term `X : bool`.

Since transporting along a path in `Type` is equivalent to applying the equivalence it came from, `X` is provably equal to `not false`, i.e. to `true`. However, upon extraction, the `Prop`-valued equality proof `bool = bool` is discarded, and we are left only with `false`.

Now we simply define a family `P : bool -> Type` for which `P true := unit` and `P false := Empty`. Since `X` is provably `true`, we can define in Coq an inhabitant of `P X`, and upon extraction this will give us a term of type `Empty`. (Thanks to Peter Lumsdaine for pointing out this improvement of my example.) Rather than supply the code, I’ll leave formalizing this as an amusing exercise.

So what *is* this term of the empty type that we get when we do the extraction? To express it, the extractor has to resort to `Obj.magic` (in the case of ML) or `unsafeCoerce` (in the case of Haskell), both of which are end-runs around the type system: they convert a value of any type to one of any other type. But even worse, the extractor actually extracts *empty types* to *unit types* for both languages — thereby sadly depriving us of the chance to find out what an inhabitant of the empty type looks like.

The point of all this silliness, of course, is that if we want to add univalence to Coq and at the same time continue to use it to develop verified software, something has to give. Specifically, the extractor should really only be throwing away terms that inhabit h-props. So if we want to use `Prop` as a syntactic marker meaning “bath-water”, then we need to enforce that all types in `Prop` are h-props — or at least ensure that it is *consistent* to suppose that they are. (We might want to use `Prop` to store type information that isn’t provably an h-prop, just as a marker to tell the extractor to throw that information away.)

And finally, *that* means that singleton elimination will no longer be valid — at least, not in the generality with which Coq currently permits it. We ought still to be able to characterize a subclass of singleton eliminations that *are* valid, including `eq` for h-sets — which applies to most data types encountered in real-world programming — but not `eq` for arbitrary types. But that’s probably another blog post.

Is there any reason to retain Prop at all? In NuPRL we just went with props-as-types, and never had a type of propositions to contend with. We did, however, have squash types to enforce proof irrelevance whenever it was appropriate to do so, and there was a delicate set of conditions under which one could eliminate out of a squashed type into another type. Of course NuPRL was an extensional type theory, so every type was an hSet, so one cannot model paths as identities in that setting, but I’m not clear on why one would need Prop in Coq, at least not for this purpose.

That’s a good question. I don’t know much about NuPRL; does it have an “extraction” feature like Coq? It seems to me (knowing very little) that you’d want to retain some sort of marker for the things that you want the extractor to forget about. I know Agda is experimenting with different sorts of “irrelevant” markers that I don’t understand very well, so I suppose something like that is an alternative to having a separate sort.

Sorry for the delay in replying, but the short answer is “yes”. NuPRL pioneered the idea of extraction from proofs, and gave the first extensions to type theory to account for proof irrelevance (they were called “subset types”, which evolved into “squash types”, which are truncations).

I agree with Bob: this sounds like one more reason to ditch Prop.

Of course, we *do* have hProp as a definable type over any given universe, so that can do at least some of the work that one might have wanted Prop for. Of course, hProp is not impredicative, but rather “stratified” by universes, in the same way that hSet and the other h-levels are.

Very good to know that Univalence and Prop are in tension in this way.

Although, we used to work with extraction (for real numbers). We are currently using Coq’s native-compute.

Full reduction at full throttle. Mathieu Boespflug, Maxime Dénès and Benjamin Grégoire in First International Conference on Certified Programs and Proofs, Tawain, December 7-9, Lecture Notes in Computer Science. Springer, 2011.

It is my impression that this is a general shift in preference.

It turns out that during evaluation we do not have easy access to the sort of a type. Hence, it is not easy do optimize the computation using the Prop-info. From this perspective, it seems to me that Prop is not so important any more.

Also, the paper states: `Functions are black boxes whose only observable behaviour is through applying it to some value, as usual.’ This form of extensionality is crucial in order to be able to use stock compilers underneath.

Finally, as emphasized by Thierry Coquand, Gandy showed that all definable functions are in fact extensional. Hence, it seems that extensionality should in fact be beneficial for fast evaluation.

Bas

I’m unconvinced.

First, Prop is to be thought as proof irrelevant. You cannot prove it internally, that’s true, but it is a technical issue rather than an essential one. Coq promises you that under no circumstance will your results depend on a proof.

Singleton elimination is not particularly typical to Prop either, it is also how Awodey/Bauer bracket types work. Not that singleton elimination is not a problem, though, as your computations may depend on the details of a proof (without any effect on the results, as long as the proof is closed). This is the reason why opaque proofs exist in Coq (and that, in turn, is the reason why it is so costly to use acc as a termination argument).

As per eq and univalence: yes, if univalence gets to be true, eq will lose most of its power, typically by being eliminated only in Prop (or perhaps in a sort of hsets). This, by the way, may be a problem with some existing uses of Coq.

As per whether Prop is useful. Well, yes. But that’s a bit short I guess. Prop is not only about extraction (though it’s certainly a nice feature of it, allowing for smooth interfacing with other programming languages), it’s really about having a sort of propositions (and hence a type of predicates and so on), in particular it allows a set of all propositions. I found this feature particularly useful (I don’t know whether epi and surjective functions are the same without such a set, for instance). That said, plenty do without a sort/set of all propositions, so it might not be necessary. But I doubt univalence is in any way a strong argument for giving Prop up.

If Coq promises me that “under no circumstance will my results depend on a proof” (by which I assume you mean an inhabitant of a type in Prop), then I think it breaks that promise with singleton elimination, as currently implemented. Under univalence, the result of transporting

falsealong a proof ofbool = booldepends on the proof. Unless by “under no circumstance” you meant “unless you assert an axiom which contradicts UIP” — and if so, then that’s exactly the point I was making: something has to give when we introduce univalence.Similarly, singleton elimination is valid for Awodey-Bauer bracket types only because they use extensional type theory (as is perfectly logical, since they are looking for models in regular 1-categories). Singleton elimination is not valid for an h-prop-valued equality under a non-extensional interpretation, as I explained above. It seems to me as though you are agreeing with this when you say “eq will lose most of its power, typically by being eliminated only in Prop” — “being eliminated only in Prop” seems to me to be the same as “no longer satisfying singleton elimination”. So what exactly are you unconvinced by?

Well, yes, you can always force the system to speak nonsense. But what I don’t find convincing is that the discrepancy between univalence and eq says anything beyond the fact that there is a discrepancy between univalence and eq. Making it an argument against Prop or singleton elimination seems quite a stretch to me. So yes, eq in presence of univalence would not be subject to singleton elimination anymore (also your example of why is perfect in term of minimality). Also: yes, Coq and univalence don’t play very well together at the moment (but I’d argue that anything asserting new elements of types out of Prop don’t play very well with Coq).

Oh, and I forgot a somewhat amusing fact. If I remember correctly, asserting excluded middle allows you to prove propositional proof irrelevance.

Peter said basically what I was going to say. You can call it a discrepancy between univalence and eq if by “eq” you mean “an inductively defined equality type, valued in a sort that we intend to be proof-irrelevant, and which satisfies singleton elimination.” But teasing apart those latter three properties allows a more nuanced statement, and lets us then ask the question, assuming that we want to include univalence (which, given that this is the homotopy type theory blog, seems like a reasonable assumption), of what else needs to be changed.

You say you agree that “eq in presence of univalence would not be subject to singleton elimination”. I assume that in this sentence by “eq” you mean only “an inductively defined equality type, valued in a sort that we intend to be proof-irrelevant”. In that case, that’s exactly what I was saying. I don’t think I concluded anything more than that; what else is there for you to be unconvinced by?

I think I misunderstood your intent then. Since we agree entirely.

Two concluding remarks: as far as we (Coq team) are aware, this is the only thing to change for univalence to be reasonable. It may or may not be an innocuous change.

There is a possibility to have eq having a degraded kind of singleton elimination. Instead of eliminating to all type (singleton elimination) or only Prop (none at all), we can arbitrarily decree that, say, Set, is a sort comprised only of hset, and then for any type A in Set, eq A is isomorphic to id A (or path A as it has come to be called in these premises) and can be eliminated freely.

Great! I’m glad we agree. Your “degraded singleton elimination” is what I was referring to when I said “we ought still to be able to characterize a subclass of singleton eliminations that are valid, including eq for h-sets”.

The only discrepancy between univalence and eq, though, comes from the facts that (a) eq is intended to be proof-irrelevant, and (b) singleton elimination holds for eq. So the conflict between univalence and eq seems exactly to come down to the fact that the current form of singleton elimination, together with proof-irrelevance for Prop, implies propositional UIP.

If one restricts singleton elimination slightly, then it’s perfectly consistent to have both a Type-valued equality “Paths”, with univalent universe(s) “Type”, and at the same time a proof-irrelevant impredicative universe “Prop”, and a Prop-valued equality “eq” (from which one can eliminate into Props but not arbitrary Types). (All these should hold, if I’m not mistaken, in the simplicial model, with Prop interpreted as hProp.)

@Harper The impredicative nature of the Prop universe appears to be essential in formulating Werner’s model of Zermelo set theory inside Coq. Not that I personally find this a compelling reason to retain Prop, but it is a reason.

I think impredicativity can be disentangled from the existence of

Prop. One could retainPropbut make it predicative, or eliminatePropbut make h-props impredicative (this is what Voevodsky seems to want). So I don’t think a desire for impredicativity weighs one way or the other on whether Coq’sPropshould be kept in a recognizable form.Peter Aczel has been advocating a “pluggable” sort of

Propthat could be “instantiated” by the user to behProp,Type,Bool, an impredicative Coq-likeProp, or anything else suitable. A more general, and radical, idea that recently occurred to me would be to refashion the handling of sorts at a more basic level to be parametric over pure type systems. That could also provide a framework for the finer-grained control of universe levels that Voevodsky seems to want with his “resizing axioms”.Bruno Barras has pointed out that univalence can do other nasty things to extraction. For instance, with univalence we can prove that

p : unit = (unit -> unit)(both are contractible). Now consider(transport p tt) tt(or, well, replace transport witheq_rectto use theProp-valued equality). Extraction discards theeq_rectand produces the application oftttott. That’s ill-typed, so the extractor inserts anObj.magic, but who knows what’ll happen when you try to execute it.Although I have not looked at the details, there are some solutions to these kind of problems in haskell. E.g. this paper develops a data type that serves as evidence for the type-checker that two types are equal.

Just to clarify my state of ignorance: if, rather than Univalence, we add an axiom for excluded middle, can we not produce a term which claims to decide the halting problem?

Actually, it’s surprising this sort of thing would claim to extract fully; if I program assuming an axiom for excluded middle, I should expect uses of that axiom to compile to code that calls an external library; only it’s one which, as it happens, can’t be implemented.

I would believe that if you asserted excluded middle in full propositions-as-types form:

Axiom PAT_LEM : forall (A : Type), A + (A -> Empty_set).

And trying to extract something that does use that gives you the message “Warning: The following axiom must be realized in the extracted code: PAT_LEM.” But I don’t think the

Prop-form of LEM could get you into any trouble:Axiom Prop_LEM : forall (P : Prop), P \/ ~P.

precisely because the inductive Prop

ordoesn’t have singleton elimination. The point here is that univalence is only used in the extracted codethroughProp, and the extractor is written so as to simply discard things in sort Prop, rather than treat them as external libraries.