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

**URL:** <https://discourse.rocq-prover.org/t/why-doesnt-coq-assume-uip-or-univalence-for-equality/1624>\
**Category:** Miscellaneous\
**Created:** [April 6, 2022, 1:08pm UTC](https://discourse.rocq-prover.org/t/why-doesnt-coq-assume-uip-or-univalence-for-equality/1624 "2022-04-06T13:08:10Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [April 6, 2022, 1:08pm UTC](https://discourse.rocq-prover.org/t/why-doesnt-coq-assume-uip-or-univalence-for-equality/1624/1 "2022-04-06T13:08:10Z")

</div>

I was learning here [Class 17: Congruence & Rewriting](https://dependenttyp.es/classes/readings/17-egraphs.html) and here [https://arxiv.org/pdf/1701.04391.pdf](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?

---

<div class="post-metadata">

**Author:** ![MSoegtrop](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@MSoegtrop](https://discourse.rocq-prover.org/u/MSoegtrop)\
**Post date:** [April 6, 2022, 1:29pm UTC](https://discourse.rocq-prover.org/t/why-doesnt-coq-assume-uip-or-univalence-for-equality/1624/2 "2022-04-06T13:29:50Z")

</div>

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

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

---

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [April 6, 2022, 1:38pm UTC](https://discourse.rocq-prover.org/t/why-doesnt-coq-assume-uip-or-univalence-for-equality/1624/3 "2022-04-06T13:38:05Z")

</div>

Interesting. In what cases is UIP provable?

---

<div class="post-metadata">

**Author:** ![MSoegtrop](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@MSoegtrop](https://discourse.rocq-prover.org/u/MSoegtrop)\
**Post date:** [April 6, 2022, 1:47pm UTC](https://discourse.rocq-prover.org/t/why-doesnt-coq-assume-uip-or-univalence-for-equality/1624/4 "2022-04-06T13:47:59Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [April 6, 2022, 2:13pm UTC](https://discourse.rocq-prover.org/t/why-doesnt-coq-assume-uip-or-univalence-for-equality/1624/5 "2022-04-06T14:13:08Z")

</div>

> [@brando90](#):
>
> 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?

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.

---

<div class="post-metadata">

**Author:** ![gares](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/gares/32/422_2.png) [@gares](https://discourse.rocq-prover.org/u/gares)\
**Post date:** [April 6, 2022, 8:36pm UTC](https://discourse.rocq-prover.org/t/why-doesnt-coq-assume-uip-or-univalence-for-equality/1624/6 "2022-04-06T20:36:18Z")

</div>

> [@brando90](#):
>
> Interesting. In what cases is UIP provable?

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](https://homotopytypetheory.org/references/hedberg/)

---

<div class="post-metadata">

**Author:** ![kyod](https://avatars.discourse-cdn.com/v4/letter/k/73ab20/32.png) [@kyod](https://discourse.rocq-prover.org/u/kyod)\
**Post date:** [April 7, 2022, 8:02am UTC](https://discourse.rocq-prover.org/t/why-doesnt-coq-assume-uip-or-univalence-for-equality/1624/7 "2022-04-07T08:02:44Z")

</div>

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.