Why doesn't Coq assume UIP or Univalence for equality?

Miscellaneous
1

I was learning here Class 17: Congruence & Rewriting and here https://arxiv.org/pdf/1701.04391.pdf that due to the dependence type theory (or ITT, not 100% the difference I assume they are the same) – that equality is not easy to define. The paper discusses a bit why but the paper makes me feel that lean assumes the axiom UIP (Uniqueness of Identity Proofs) anyway.

Why does Coq assume UIP or Univalence so that equality is well defined? Is the extra flexibility actually needed? Especially in practice? e.g. formalization of mathematics or program verification? When is this inconvenience truly needed? Why does lean need it but coq does not?

2

In my experience UIP is rarely needed - especially in program verification. The reason is that most types one handles in program verification have decidable equality, and for types with decidable equality UIP can be proven without axioms. See

Classical_Prop.EqdepTheory.UIP
	 : forall (U : Type) (x y : U) (p1 p2 : x = y), p1 = p2

Eqdep_dec.eq_proofs_unicity
	 : forall A : Type,
       (forall x y : A, x = y \/ x <> y) ->
       forall (x y : A) (p1 p2 : x = y), p1 = p2

The first is the UIP axiom, the second is a theorem in the standard library (which doesn’t use axioms).

I guess the reason it is not assumed by default is that it is not compatible (mutually consistent) with some other axioms one might want to use - but don’t ask me which.

3

Interesting. In what cases is UIP provable?

4

The lemma says that decidable equality is sufficient - this includes e.g. Z or functions from finite types (like 64 bit integers) to types with decidable equality and a lot of other common types. The decidability of equality need not be practical - as in the case of functions from 64 bit integers to a decidable type - it is sufficient that there is a proof for decidability. So this covers quite a lot. The most prominent types without decidable equality are R and functions from non-finite types, like a function Z → Z.

I am not a computer scientist (physicist) so I don’t know if there are other cases in which UIP is provable - I am not aware of any.

1 Like
5

Coq assumes neither UIP nor univalence by default; Coq libraries can declare the postulates and you can choose to use one or the other. Lean just chooses UIP for you and does not support univalence.

6

It is for the types which have a decidable equality, and only them.
Here the reference, and a short summary of it: Hedberg: A coherence theorem for Martin-Löf type theory | Homotopy Type Theory

1 Like
7

Additionally, you can prove that certain class of types satisfy UIP if you assume univalence, for instance any (homotopy-)proposition, meaning a type where every two elements are equal, satisfy UIP and the type of h-propositions itself satisfy UIP (because equality of propositions is equivallent to bi-implication under univalence). These examples are treated in the HoTT Book.