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.
Homotopy Type Theory 
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 false along a proof of bool = bool depends 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.
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.)
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”.
@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 retain Prop but make it predicative, or eliminate Prop but 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’s Prop should be kept in a recognizable form.
Peter Aczel has been advocating a “pluggable” sort of Prop that could be “instantiated” by the user to be hProp, Type, Bool, an impredicative Coq-like Prop, 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 with eq_rect to use the Prop-valued equality). Extraction discards the eq_rect and produces the application of tt to tt. That’s ill-typed, so the extractor inserts an Obj.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 or doesn’t have singleton elimination. The point here is that univalence is only used in the extracted code through Prop, and the extractor is written so as to simply discard things in sort Prop, rather than treat them as external libraries.