<p>This is a hard question to answer, in part because it's unclear what it means to get something "by accident". Regularly, though, people run into the <code>Universe Inconsistency</code> error of Coq, as some quick googling will show (e.g. <a href="https://groups.google.com/forum/#!topic/homotopytypetheory/ljBz8cYkfkY">here</a>). This certainly sometimes happens by accident, sometimes in the attempt at showing inconsistencies or testing the limits of the prover.</p>

<p>One of the big sources of universe inconsistencies unsurprisingly comes from trying to formalize category theory in Coq, as is mentioned in <a href="http://arxiv.org/pdf/1401.7694">this article</a> by Gross, Chlipala and Spivak.</p>

<p>In most cases, it's hard to tell whether the inconsistency comes from an actually inconsistent statement, or just a limitation of the proof checker, which sometimes has counter-intuitive restrictions on universes, particularly in the allowed parameters for inductive types. This is actually a somewhat tricky subject (see the <a href="https://coq.inria.fr/refman/Reference-Manual006.html#Cic-inductive-definitions">official definition</a> and Chlipala's more accessible <a href="http://adam.chlipala.net/cpdt/html/Universes.html">discussion</a>).</p>

CC BY-SA 3.0
2016-02-24T19:38:12.263Z
2016-02-24T19:38:12.263Z
cody
<p>In dependent types, <code>Type : Type</code> results in inconsistency (Girard's or Hurken's paradox). </p>

<p>Are there examples of universe inconsistency (where assuming <code>Type : Type</code> would result something that is false) showing up "accidentally" when not deliberately trying to prove it (when proving unrelated things)?</p>

<type-theory><coq><dependent-type>
Examples of Universe inconsistency in normal use of dependent types
fread2281
# Examples of Universe inconsistency in normal use of dependent types

(Asked by: username_0 on 2016-02-24)

In dependent types, `Type : Type` results in inconsistency (Girard's or Hurken's paradox).

Are there examples of universe inconsistency (where assuming `Type : Type` would result something that is false) showing up "accidentally" when not deliberately trying to prove it (when proving unrelated things)?

**Tags:** type-theory, coq, dependent-type

---

## 1 answers

### Answer by username_1 on 2016-02-24. Score: 9 | Accepted answer

This is a hard question to answer, in part because it's unclear what it means to get something "by accident". Regularly, though, people run into the `Universe Inconsistency` error of Coq, as some quick googling will show (e.g. [here](https://groups.google.com/forum/#!topic/homotopytypetheory/ljBz8cYkfkY)). This certainly sometimes happens by accident, sometimes in the attempt at showing inconsistencies or testing the limits of the prover.

One of the big sources of universe inconsistencies unsurprisingly comes from trying to formalize category theory in Coq, as is mentioned in [this article](http://arxiv.org/pdf/1401.7694) by Gross, Chlipala and Spivak.

In most cases, it's hard to tell whether the inconsistency comes from an actually inconsistent statement, or just a limitation of the proof checker, which sometimes has counter-intuitive restrictions on universes, particularly in the allowed parameters for inductive types. This is actually a somewhat tricky subject (see the [official definition](https://coq.inria.fr/refman/Reference-Manual006.html#Cic-inductive-definitions) and Chlipala's more accessible [discussion](http://adam.chlipala.net/cpdt/html/Universes.html)).


---

