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.